Theorem biimpr 222

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 215	. 2 ⊢ ((𝜑 ↔ 𝜓) ↔ ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)))
2		simprim 168	. 2 ⊢ (¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → (𝜓 → 𝜑))
3	1, 2	sylbi 219	1 ⊢ ((𝜑 ↔ 𝜓) → (𝜓 → 𝜑))

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

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 209

This theorem is referenced by:  bicom1  223  pm5.74  272  bija  384  simplbi2comt  504  pm4.72  946  bianir  1053  albi  1815  spsbbi  2074  cbv2w  2353  cbv2  2419  cbv2h  2422  equvel  2475  dfeumo  2615  eu6  2655  2eu6  2740  ralbi  3167  ceqsalt  3527  vtoclgft  3553  euind  3714  reu6  3716  reuind  3743  sbciegft  3807  axprALT  5322  axpr  5328  iota4  6335  fv3  6687  nn0prpwlem  33670  nn0prpw  33671  bj-animbi  33894  bj-bi3ant  33923  bj-cbv2hv  34119  bj-ceqsalt0  34200  bj-ceqsalt1  34201  bj-bm1.3ii  34356  dfgcd3  34604  tsbi3  35412  mapdrvallem2  38780  axc11next  40736  pm13.192  40740  exbir  40810  con5  40854  sbcim2g  40870  trsspwALT  41150  trsspwALT2  41151  sspwtr  41153  sspwtrALT  41154  pwtrVD  41156  pwtrrVD  41157  snssiALTVD  41159  sstrALT2VD  41166  sstrALT2  41167  suctrALT2VD  41168  eqsbc3rVD  41172  simplbi2VD  41178  exbirVD  41185  exbiriVD  41186  imbi12VD  41205  sbcim2gVD  41207  simplbi2comtVD  41220  con5VD  41232  2uasbanhVD  41243  absnsb  43261