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 277 nakui 278 gonaii 300 onaii 306 jonaii 310 gihonaii 314 pameii 329 gripaui 334 ckajii 346 ckinii 351 simsai 359 dunlii 368 mintui 376 stecii 384 muplii 389 muplili 390 mupliiri 391 simxui 396 tei 400 te-dual 403 te-dual-l 404 te-dual-r 405 cei 410 subi 450 poi-roi 472 ro-quanti 478 kampui 485 johei 489 kuhai 493 selbrii 504 fatcii 508 niblii 513 fahui 530 taknii 541 pa-dai 559 poi-pai 563 pomboi 567 sezni-elt 577 dugrii 629 jompaui 653 kuzypaui 657 kihirnihi-antisym 698 frinynahu-kacnahul 707 frinynahu-kacnahur 708 fancui 730