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 269 lnc 276 nakuri 280 gonairi 303 onairi 307 jonairi 311 gihonairi 315 gripauri 335 ckajiri 347 ckiniri 352 simsari 362 dunliri 369 minturi 377 steciri 385 mupliri 392 muplirii 393 simxuri 397 teri 401 te-dual 403 te-dual-l 404 te-dual-r 405 ceri 411 wit 425 bi-revg 438 subt 463 zilcmi-nomei 466 cmima-zilcmi 467 selcmi-zilcmi 468 poi-rori 473 ro-quantri 479 kampuri 486 joheri 490 kuhari 494 selbriri 505 fatciri 509 nibliri 515 fahuri 533 kinfiri 544 kinrari 547 pa-dari 560 poi-pari 564 pombori 568 sumji-no 611 pilji-no 618 dugriri 630 jompauri 654 kuzypauri 658 kihirnihi-refl 692 kihirduhi-refl 697 kihirnihi-antisym 698