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

Theorem biimpr 210
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 203 . 2 ((𝜑𝜓) ↔ ¬ ((𝜑𝜓) → ¬ (𝜓𝜑)))
2 simprim 162 . 2 (¬ ((𝜑𝜓) → ¬ (𝜓𝜑)) → (𝜓𝜑))
31, 2sylbi 207 1 ((𝜑𝜓) → (𝜓𝜑))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196
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 197
This theorem is referenced by:  bicom1  211  pm5.74  259  bija  369  simplbi2comt  657  pm4.72  956  bianir  1047  albi  1895  cbv2h  2414  equvel  2484  euex  2631  2eu6  2696  ceqsalt  3368  euind  3534  reu6  3536  reuind  3552  sbciegft  3607  axpr  5054  iota4  6030  fv3  6367  nn0prpwlem  32623  nn0prpw  32624  bj-bi3ant  32880  bj-ssbbi  32928  bj-cbv2hv  33037  bj-ceqsalt0  33179  bj-ceqsalt1  33180  dfgcd3  33481  tsbi3  34255  mapdrvallem2  37436  axc11next  39109  pm13.192  39113  exbir  39186  con5  39230  sbcim2g  39250  trsspwALT  39547  trsspwALT2  39548  sspwtr  39550  sspwtrALT  39551  pwtrVD  39558  pwtrrVD  39559  snssiALTVD  39561  sstrALT2VD  39568  sstrALT2  39569  suctrALT2VD  39570  eqsbc3rVD  39574  simplbi2VD  39580  exbirVD  39587  exbiriVD  39588  imbi12VD  39608  sbcim2gVD  39610  simplbi2comtVD  39623  con5VD  39635  2uasbanhVD  39646
  Copyright terms: Public domain W3C validator