bi-rev - brismu bridi

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

Theorem bi-rev 70

Description: Modus ponens in the other direction. Theorem mpbir in [ILE] p. 0. (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 66	. 2 ⊢ go broda gi brode
4	1, 3	bi 69	1 ⊢ brode

Colors of variables: sumti selbri bridi

This theorem was proved from axioms: ax-mp 10 ax-k 11 ax-s 14 ax-ge-le 34 ax-ge-re 35 ax-ge-in 36

This theorem depends on definitions: df-go 52

This theorem is referenced by: naari 81 anairi 87 najari 92 janairi 98 nagihari 103 gihanairi 108 eri 117 jeri 121 giheri 125 gari 131 ari 141 jari 147 gihari 151 ori 155 jori 162 gihori 166 seri 170 duri 200 ceihi 208 lnc 213 nakuri 217 gonairi 229 onairi 233 jonairi 237 gihonairi 241 gripauri 260 ckajiri 272 ckiniri 277 simsari 287 dunliri 294 minturi 301 steciri 309 mupliri 316 muplirii 317 simxuri 321 teri 325 te-dual 327 te-dual-l 328 te-dual-r 329 ceri 335 wit 348 bi-revg 358 zilcmi-nomei 368 cmima-zilcmi 369 poi-rori 374 ro-quantri 380 kampuri 386 joheri 390 kuhari 394 fatciri 407 nibliri 413 fahuri 431 kinfiri 441 kinrari 444 pa-dari 457 poi-pari 461 sumji-no 501 pilji-no 508 dugriri 518 jompauri 537 kuzypauri 541 kihirnihi-refl 566