bi - brismu bridi

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

Theorem bi 69

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 54	. 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 34

This theorem depends on definitions: df-go 52

This theorem is referenced by: bi-rev 70 naai 79 anaii 85 najai 90 janaii 96 nagihai 101 gihanaii 106 ei 116 jei 120 gihei 124 gai 129 ga-lin 132 ga-rin 133 ai 140 a-comi 143 jai 146 gihai 150 oi 154 o-comi 157 joi 161 gihoi 165 sei 169 dui 198 duis 199 lnci 214 nakui 215 gonaii 226 onaii 232 jonaii 236 gihonaii 240 pameii 254 gripaui 259 ckajii 271 ckinii 276 simsai 284 dunlii 293 mintui 300 stecii 308 muplii 313 muplili 314 mupliiri 315 simxui 320 tei 324 te-dual 327 te-dual-l 328 te-dual-r 329 cei 334 subi 351 poi-roi 373 ro-quanti 379 kampui 385 johei 389 kuhai 393 fatcii 406 niblii 411 fahui 428 taknii 438 pa-dai 456 poi-pai 460 sezni-elt 468 dugrii 517 jompaui 536 kuzypaui 540 fancui 575