Theorem hirstL-ax3

Description: The third axiom of a system called "L" but proven to be a theorem since set.mm uses a different third axiom. This is named hirst after Holly P. Hirst and Jeffry L. Hirst. Axiom A3 of Mendelson p. 35. (Contributed by Jarvin Udandy, 7-Feb-2015) (Proof modification is discouraged.)

	Ref	Expression
Assertion	hirstL-ax3	⊢ ( ( ¬ 𝜑 → ¬ 𝜓 ) → ( ( ¬ 𝜑 → 𝜓 ) → 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		pm4.64	⊢ ( ( ¬ 𝜑 → 𝜓 ) ↔ ( 𝜑 ∨ 𝜓 ) )
2		pm4.66	⊢ ( ( ¬ 𝜑 → ¬ 𝜓 ) ↔ ( 𝜑 ∨ ¬ 𝜓 ) )
3		pm2.64	⊢ ( ( 𝜑 ∨ 𝜓 ) → ( ( 𝜑 ∨ ¬ 𝜓 ) → 𝜑 ) )
4	3	com12	⊢ ( ( 𝜑 ∨ ¬ 𝜓 ) → ( ( 𝜑 ∨ 𝜓 ) → 𝜑 ) )
5	2 4	sylbi	⊢ ( ( ¬ 𝜑 → ¬ 𝜓 ) → ( ( 𝜑 ∨ 𝜓 ) → 𝜑 ) )
6	1 5	biimtrid	⊢ ( ( ¬ 𝜑 → ¬ 𝜓 ) → ( ( ¬ 𝜑 → 𝜓 ) → 𝜑 ) )