bi - brismu bridi

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

Theorem bi 101

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 85	. 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 48

This theorem depends on definitions: df-go 83

This theorem is referenced by: bi-rev 102 naai 111 anaii 117 najai 122 janaii 128 nagihai 133 gihanaii 138 ei 148 jei 153 gihei 157 gai 162 ga-lin 165 ga-rin 166 ai 185 a-comi 188 jai 191 gihai 195 oi 199 o-comi 202 joi 206 gihoi 210 sei 214 big1 226 dui 252 duis 253 lnci 276 nakui 277 gonaii 299 onaii 305 jonaii 309 gihonaii 313 pameii 328 gripaui 333 ckajii 345 ckinii 350 simsai 358 dunlii 367 mintui 374 stecii 382 muplii 387 muplili 388 mupliiri 389 simxui 394 tei 398 te-dual 401 te-dual-l 402 te-dual-r 403 cei 408 subi 448 poi-roi 466 ro-quanti 472 kampui 479 johei 483 kuhai 487 selbrii 498 fatcii 502 niblii 507 fahui 524 taknii 535 pa-dai 553 poi-pai 557 pomboi 561 sezni-elt 571 dugrii 621 jompaui 640 kuzypaui 644 kihirnihi-antisym 685 fancui 703