Theorem bi2 189

Description: Property of the biconditional connective. (Contributed by NM, 11-May-1999.) (Proof shortened by Wolf Lammen, 11-Nov-2012.)

Assertion

Ref	Expression
bi2	⊢ ((φ ↔ ψ) → (ψ → φ))

Proof of Theorem bi2

Step	Hyp	Ref	Expression
1		dfbi1 184	. 2 ⊢ ((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ)))
2		simprim 142	. 2 ⊢ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (ψ → φ))
3	1, 2	sylbi 187	1 ⊢ ((φ ↔ ψ) → (ψ → φ))

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

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 177

This theorem is referenced by:  bicom1  190  pm5.74  235  bi3ant  280  bija  344  pm4.72  846  exbir  1365  simplbi2comg  1373  albi  1564  exbi  1581  cbv2h  1980  sbied  2036  2eu6  2289  ceqsalt  2882  euind  3024  reu6  3026  reuind  3040  sbciegft  3077  iota4  4358  fv3  5342