Theorem biimpr 220

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 213	. 2 ⊢ ((𝜑 ↔ 𝜓) ↔ ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)))
2		simprim 166	. 2 ⊢ (¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → (𝜓 → 𝜑))
3	1, 2	sylbi 217	1 ⊢ ((𝜑 ↔ 𝜓) → (𝜓 → 𝜑))

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

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 207

This theorem is referenced by:  bicom1  221  pm5.74  270  bija  380  simplbi2comt  501  pm4.72  951  bianir  1058  albi  1818  spsbbi  2073  cbv2w  2338  cbv2  2407  cbv2h  2410  equvel  2460  dfeumo  2536  eu6  2573  2eu6  2656  ralbi  3092  rexbi  3093  ceqsal1t  3493  elabgt  3651  elabgtOLD  3652  euind  3707  reu6  3709  reuind  3736  sbciegftOLD  3803  sepex  5270  axprALT  5392  axprOLD  5401  iota4  6512  fv3  6894  fineqvpow  35127  nn0prpwlem  36340  nn0prpw  36341  bj-animbi  36577  bj-bi3ant  36607  bj-cbv2hv  36815  bj-ceqsalt0  36902  bj-ceqsalt1  36903  bj-bm1.3ii  37082  dfgcd3  37342  tsbi3  38159  mapdrvallem2  41664  eu6w  42699  axc11next  44430  pm13.192  44434  exbir  44504  con5  44547  sbcim2g  44563  trsspwALT  44842  trsspwALT2  44843  sspwtr  44845  sspwtrALT  44846  pwtrVD  44848  pwtrrVD  44849  snssiALTVD  44851  sstrALT2VD  44858  sstrALT2  44859  suctrALT2VD  44860  eqsbc2VD  44864  simplbi2VD  44870  exbirVD  44877  exbiriVD  44878  imbi12VD  44897  sbcim2gVD  44899  simplbi2comtVD  44912  con5VD  44924  2uasbanhVD  44935  nimnbi2  45188  absnsb  47056  thincciso  49339