bi - brismu bridi

	brismu bridi		< Previous Next > Nearby theorems
Mirrors > Home > Home > Th. List > bi

Theorem bi 79

Description: Like modus ponens ax-mp 10 but for biconditionals. (Contributed by la korvo, 16-Jul-2023.)

**Hypotheses**
Ref	Expression
bi.0	⊢ broda
bi.1	⊢ go broda gi brode

**Assertion**
Ref	Expression
bi	⊢ brode

**Proof of Theorem bi**
Step	Hyp	Ref	Expression
1		bi.0	. 2 ⊢ broda
2		bi.1	. . 3 ⊢ go broda gi brode
3	2	go-ganai 63	. 2 ⊢ ganai broda gi brode
4	1, 3	ax-mp 10	1 ⊢ brode

Colors of variables: sumti selbri bridi

This theorem was proved from axioms: ax-mp 10 ax-ge-le 43

This theorem depends on definitions: df-go 61

This theorem is referenced by: bi-rev 80 naai 89 anaii 95 najai 100 janaii 106 nagihai 111 gihanaii 116 ei 126 jei 130 gihei 134 gai 139 ga-lin 142 ga-rin 143 ai 154 a-comi 157 jai 160 gihai 164 oi 168 o-comi 171 joi 175 gihoi 179 sei 183 dui 216 duis 217 lnci 240 nakui 241 gonaii 262 onaii 268 jonaii 272 gihonaii 276 pameii 291 gripaui 296 ckajii 308 ckinii 313 simsai 321 dunlii 330 mintui 337 stecii 345 muplii 350 muplili 351 mupliiri 352 simxui 357 tei 361 te-dual 364 te-dual-l 365 te-dual-r 366 cei 371 subi 390 poi-roi 414 ro-quanti 420 kampui 427 johei 431 kuhai 435 selbrii 446 fatcii 450 niblii 455 fahui 472 taknii 482 pa-dai 500 poi-pai 504 sezni-elt 514 dugrii 563 jompaui 582 kuzypaui 586 fancui 632