bi-rev - brismu bridi

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

Theorem bi-rev 102

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 98	. 2 ⊢ go broda gi brode
4	1, 3	bi 101	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 48 ax-ge-re 49 ax-ge-in 50

This theorem depends on definitions: df-go 83

This theorem is referenced by: naari 113 anairi 119 najari 124 janairi 130 nagihari 135 gihanairi 140 eri 149 jeri 154 giheri 158 gari 164 ari 186 jari 192 gihari 196 ori 200 jori 207 gihori 211 seri 215 duri 254 ceihi 268 lnc 275 nakuri 279 gonairi 302 onairi 306 jonairi 310 gihonairi 314 gripauri 334 ckajiri 346 ckiniri 351 simsari 361 dunliri 368 minturi 375 steciri 383 mupliri 390 muplirii 391 simxuri 395 teri 399 te-dual 401 te-dual-l 402 te-dual-r 403 ceri 409 wit 423 bi-revg 436 subt 458 zilcmi-nomei 461 cmima-zilcmi 462 poi-rori 467 ro-quantri 473 kampuri 480 joheri 484 kuhari 488 selbriri 499 fatciri 503 nibliri 509 fahuri 527 kinfiri 538 kinrari 541 pa-dari 554 poi-pari 558 pombori 562 sumji-no 605 pilji-no 612 dugriri 622 jompauri 641 kuzypauri 645 kihirnihi-refl 679 kihirduhi-refl 684 kihirnihi-antisym 685