MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  biimpr Structured version   Visualization version   GIF version

Theorem biimpr 211
Description: Property of the biconditional connective. (Contributed by NM, 11-May-1999.) (Proof shortened by Wolf Lammen, 11-Nov-2012.)
Assertion
Ref Expression
biimpr ((𝜑𝜓) → (𝜓𝜑))

Proof of Theorem biimpr
StepHypRef Expression
1 dfbi1 204 . 2 ((𝜑𝜓) ↔ ¬ ((𝜑𝜓) → ¬ (𝜓𝜑)))
2 simprim 163 . 2 (¬ ((𝜑𝜓) → ¬ (𝜓𝜑)) → (𝜓𝜑))
31, 2sylbi 208 1 ((𝜑𝜓) → (𝜓𝜑))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197
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 198
This theorem is referenced by:  bicom1  212  pm5.74  261  bija  371  simplbi2comt  491  pm4.72  963  bianir  1074  albi  1903  cbv2h  2444  equvel  2507  euex  2667  2eu6  2733  ceqsalt  3433  euind  3602  reu6  3604  reuind  3620  sbciegft  3675  axpr  5108  iota4  6092  fv3  6436  nn0prpwlem  32660  nn0prpw  32661  bj-bi3ant  32911  bj-ssbbi  32960  bj-cbv2hv  33067  bj-ceqsalt0  33200  bj-ceqsalt1  33201  bj-bm1.3ii  33353  dfgcd3  33506  tsbi3  34271  mapdrvallem2  37444  axc11next  39124  pm13.192  39128  exbir  39200  con5  39244  sbcim2g  39264  trsspwALT  39560  trsspwALT2  39561  sspwtr  39563  sspwtrALT  39564  pwtrVD  39571  pwtrrVD  39572  snssiALTVD  39574  sstrALT2VD  39581  sstrALT2  39582  suctrALT2VD  39583  eqsbc3rVD  39587  simplbi2VD  39593  exbirVD  39600  exbiriVD  39601  imbi12VD  39621  sbcim2gVD  39623  simplbi2comtVD  39636  con5VD  39648  2uasbanhVD  39659  absnsb  41669
  Copyright terms: Public domain W3C validator