Theorem bi3 150

Description: Property of the biconditional connective.

Assertion

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

Proof of Theorem bi3

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

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

This theorem is referenced by:  impbi 157  bii 158  asymref2 3432

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