Theorem biimpr 219

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

Step	Hyp	Ref	Expression
1		dfbi1 212	. 2 ⊢ ((𝜑 ↔ 𝜓) ↔ ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)))
2		simprim 166	. 2 ⊢ (¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → (𝜓 → 𝜑))
3	1, 2	sylbi 216	1 ⊢ ((𝜑 ↔ 𝜓) → (𝜓 → 𝜑))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  bicom1  220  pm5.74  270  bija  380  simplbi2comt  501  pm4.72  948  bianir  1057  albi  1813  spsbbi  2069  cbv2w  2328  cbv2  2397  cbv2h  2400  equvel  2450  dfeumo  2526  eu6  2563  2eu6  2647  ralbi  3098  rexbi  3099  ceqsal1t  3500  elabgt  3658  elabgtOLD  3659  euind  3717  reu6  3719  reuind  3746  sbciegft  3812  axprALT  5416  axpr  5422  iota4  6523  fv3  6909  fineqvpow  34652  nn0prpwlem  35742  nn0prpw  35743  bj-animbi  35970  bj-bi3ant  36002  bj-cbv2hv  36210  bj-ceqsalt0  36298  bj-ceqsalt1  36299  bj-bm1.3ii  36479  dfgcd3  36739  tsbi3  37543  mapdrvallem2  41055  axc11next  43766  pm13.192  43770  exbir  43840  con5  43884  sbcim2g  43900  trsspwALT  44180  trsspwALT2  44181  sspwtr  44183  sspwtrALT  44184  pwtrVD  44186  pwtrrVD  44187  snssiALTVD  44189  sstrALT2VD  44196  sstrALT2  44197  suctrALT2VD  44198  eqsbc2VD  44202  simplbi2VD  44208  exbirVD  44215  exbiriVD  44216  imbi12VD  44235  sbcim2gVD  44237  simplbi2comtVD  44250  con5VD  44262  2uasbanhVD  44273  nimnbi2  44459  absnsb  46332  thincciso  47978