Theorem bi2 131

Description: Property of the biconditional connective.

Assertion

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

Proof of Theorem bi2

Step	Hyp	Ref	Expression
1		df-bi 128	. . 3 ⊢ ¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ)))
2		pm3.26im 120	. . 3 ⊢ (¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ))) → ((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))))
3	1, 2	ax-mp 6	. 2 ⊢ ((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ)))
4		pm3.27im 121	. 2 ⊢ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (ψ → φ))
5	3, 4	syl 12	1 ⊢ ((φ ↔ ψ) → (ψ → φ))

Syntax hints:  ¬ wn 1   → wi 2   ↔ wb 127

This theorem is referenced by:  biimpr 134  biimprd 136  bii 140  pm5.74 442  pm4.72 485  tbt 541  pclem6 555  19.15 694  19.18 732  cbv2 846  sbied 903  fv3 2839

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

This theorem depends on definitions:  df-bi 128

metamath.org