Theorem bi2 149

Description: Property of the biconditional connective.

Assertion

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

Proof of Theorem bi2

Step	Hyp	Ref	Expression
1		df-bi 147	. . 3 ⊢ ¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ)))
2		pm3.26im 139	. . 3 ⊢ (¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ))) → ((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))))
3	1, 2	ax-mp 7	. 2 ⊢ ((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ)))
4		pm3.27im 140	. 2 ⊢ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (ψ → φ))
5	3, 4	syl 10	1 ⊢ ((φ ↔ ψ) → (ψ → φ))

Syntax hints:  ¬ wn 2   → wi 3   ↔ wb 146

This theorem is referenced by:  biimpr 152  biimprd 154  bii 158  pm5.74 582  pm4.72 640  pclem6 740  pm5.75 748  19.15 995  19.18 1048  cbv2 1161  sbied 1193  2eu6 1452  reu3 1927  sbciegft 1955  axpr 2774  fv3 3735

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147

Copyright terms: Public domain