Theorem bi3 132

Description: Property of the biconditional connective.

Assertion

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

Proof of Theorem bi3

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

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

This theorem is referenced by:  impbi 139  bii 140

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