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  269  bija  379  simplbi2comt  500  pm4.72  947  bianir  1056  albi  1812  spsbbi  2068  cbv2w  2328  cbv2  2397  cbv2h  2400  equvel  2450  dfeumo  2526  eu6  2563  2eu6  2647  ralbi  3099  rexbi  3100  ceqsal1t  3502  elabgt  3660  elabgtOLD  3661  euind  3719  reu6  3721  reuind  3748  sbciegftOLD  3815  axprALT  5424  axpr  5430  iota4  6532  fv3  6918  fineqvpow  34721  nn0prpwlem  35811  nn0prpw  35812  bj-animbi  36039  bj-bi3ant  36071  bj-cbv2hv  36279  bj-ceqsalt0  36367  bj-ceqsalt1  36368  bj-bm1.3ii  36548  dfgcd3  36808  tsbi3  37613  mapdrvallem2  41122  axc11next  43846  pm13.192  43850  exbir  43920  con5  43964  sbcim2g  43980  trsspwALT  44260  trsspwALT2  44261  sspwtr  44263  sspwtrALT  44264  pwtrVD  44266  pwtrrVD  44267  snssiALTVD  44269  sstrALT2VD  44276  sstrALT2  44277  suctrALT2VD  44278  eqsbc2VD  44282  simplbi2VD  44288  exbirVD  44295  exbiriVD  44296  imbi12VD  44315  sbcim2gVD  44317  simplbi2comtVD  44330  con5VD  44342  2uasbanhVD  44353  nimnbi2  44539  absnsb  46411  thincciso  48106