Theorem bi1 130

Description: Property of the biconditional connective.

Assertion

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

Proof of Theorem bi1

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

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

This theorem is referenced by:  biimp 133  biimpd 135  bii 140  pm5.74 442  ibib 448  pm4.71 481  nbn 542  pclem6 555  19.15 694  19.18 732  cbv2 846  sbied 903  eumo0 1022  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