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 415 ro-quanti 421 kampui 427 johei 431 kuhai 435 fatcii 448 niblii 453 fahui 470 taknii 480 pa-dai 498 poi-pai 502 sezni-elt 510 dugrii 559 jompaui 578 kuzypaui 582 fancui 628