bi-rev - brismu bridi

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

Theorem bi-rev 80

Description: Modus ponens in the other direction. (Contributed by la korvo, 16-Jul-2023.)

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

**Assertion**
Ref	Expression
bi-rev	⊢ brode

**Proof of Theorem bi-rev**
Step	Hyp	Ref	Expression
1		bi-rev.0	. 2 ⊢ broda
2		bi-rev.1	. . 3 ⊢ go brode gi broda
3	2	go-comi 76	. 2 ⊢ go broda gi brode
4	1, 3	bi 79	1 ⊢ brode

Colors of variables: sumti selbri bridi

This theorem was proved from axioms: ax-mp 10 ax-k 11 ax-s 15 ax-ge-le 43 ax-ge-re 44 ax-ge-in 45

This theorem depends on definitions: df-go 61

This theorem is referenced by: naari 91 anairi 97 najari 102 janairi 108 nagihari 113 gihanairi 118 eri 127 jeri 131 giheri 135 gari 141 ari 155 jari 161 gihari 165 ori 169 jori 176 gihori 180 seri 184 duri 218 ceihi 232 lnc 239 nakuri 243 gonairi 265 onairi 269 jonairi 273 gihonairi 277 gripauri 297 ckajiri 309 ckiniri 314 simsari 324 dunliri 331 minturi 338 steciri 346 mupliri 353 muplirii 354 simxuri 358 teri 362 te-dual 364 te-dual-l 365 te-dual-r 366 ceri 372 wit 386 bi-revg 397 zilcmi-nomei 409 cmima-zilcmi 410 poi-rori 415 ro-quantri 421 kampuri 428 joheri 432 kuhari 436 selbriri 447 fatciri 451 nibliri 457 fahuri 475 kinfiri 485 kinrari 488 pa-dari 501 poi-pari 505 sumji-no 547 pilji-no 554 dugriri 564 jompauri 583 kuzypauri 587 kihirnihi-refl 612