Mathbox for Richard Penner < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ifpimim Structured version   Unicode version

Theorem ifpimim 35852
 Description: Consequnce of implication. (Contributed by RP, 17-Apr-2020.)
Assertion
Ref Expression
ifpimim if- if- if-

Proof of Theorem ifpimim
StepHypRef Expression
1 pm2.521 157 . . . . . 6
21orim1i 519 . . . . 5
32adantr 466 . . . 4
4 id 23 . . . . . 6
54orci 391 . . . . 5
65a1i 11 . . . 4
73, 6jca 534 . . 3
84orci 391 . . . . 5
98a1i 11 . . . 4
10 simpr 462 . . . 4
119, 10jca 534 . . 3
127, 11jca 534 . 2
13 pm4.81 367 . . . . 5
1413bicomi 205 . . . 4
15 ifpbi1 35820 . . . 4 if- if-
1614, 15ax-mp 5 . . 3 if- if-
17 dfifp4 1424 . . 3 if-
1816, 17bitri 252 . 2 if-
19 ifpim123g 35843 . 2 if- if-
2012, 18, 193imtr4i 269 1 if- if- if-
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 187   wo 369   wa 370  if-wif 1420 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-ifp 1421 This theorem is referenced by:  frege58acor  36109  frege60a  36111  frege65a  36116
 Copyright terms: Public domain W3C validator