Axiom ax-luk2

Description: 2 of 3 axioms for propositional calculus due to Lukasiewicz. Copy of luk-2 or pm2.18 , but introduced as an axiom. The core idea behind this axiom is, that if something can be implied from both an antecedent, and separately from its negation, then the antecedent is irrelevant to the consequent, and can safely be dropped. This is perhaps better seen from the following slightly extended version (related to pm2.65 ):

( ( ph -> ph ) -> ( ( -. ph -> ph ) -> ph ) ) . (Contributed by Wolf Lammen, 17-Dec-2018) (New usage is discouraged.)

	Ref	Expression
Assertion	ax-luk2	⊢ ( ( ¬ 𝜑 → 𝜑 ) → 𝜑 )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		wph	⊢ 𝜑
1	0	wn	⊢ ¬ 𝜑
2	1 0	wi	⊢ ( ¬ 𝜑 → 𝜑 )
3	2 0	wi	⊢ ( ( ¬ 𝜑 → 𝜑 ) → 𝜑 )