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

Theorem biimpr 223
 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 216 . 2 ((𝜑𝜓) ↔ ¬ ((𝜑𝜓) → ¬ (𝜓𝜑)))
2 simprim 169 . 2 (¬ ((𝜑𝜓) → ¬ (𝜓𝜑)) → (𝜓𝜑))
31, 2sylbi 220 1 ((𝜑𝜓) → (𝜓𝜑))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209 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 210 This theorem is referenced by:  bicom1  224  pm5.74  273  bija  385  simplbi2comt  505  pm4.72  947  bianir  1054  albi  1820  spsbbi  2078  cbv2w  2358  cbv2  2424  cbv2h  2427  equvel  2480  dfeumo  2619  eu6  2658  2eu6  2743  ralbi  3159  ceqsalt  3502  vtoclgft  3528  euind  3690  reu6  3692  reuind  3719  sbciegft  3783  axprALT  5300  axpr  5306  iota4  6315  fv3  6670  nn0prpwlem  33744  nn0prpw  33745  bj-animbi  33968  bj-bi3ant  33997  bj-cbv2hv  34195  bj-ceqsalt0  34285  bj-ceqsalt1  34286  bj-bm1.3ii  34442  dfgcd3  34699  tsbi3  35532  mapdrvallem2  38900  axc11next  41045  pm13.192  41049  exbir  41119  con5  41163  sbcim2g  41179  trsspwALT  41459  trsspwALT2  41460  sspwtr  41462  sspwtrALT  41463  pwtrVD  41465  pwtrrVD  41466  snssiALTVD  41468  sstrALT2VD  41475  sstrALT2  41476  suctrALT2VD  41477  eqsbc3rVD  41481  simplbi2VD  41487  exbirVD  41494  exbiriVD  41495  imbi12VD  41514  sbcim2gVD  41516  simplbi2comtVD  41529  con5VD  41541  2uasbanhVD  41552  absnsb  43559
 Copyright terms: Public domain W3C validator