This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY Other axiomatizations related to classical propositional calculus Derive the standard axioms from the Lukasiewicz axioms luklem5
Description: Used to rederive standard propositional axioms from Lukasiewicz'.
(Contributed by NM , 22-Dec-2002) (Proof modification is discouraged.)
(New usage is discouraged.)
Ref
Expression
Assertion
luklem5 ⊢ ( 𝜑 → ( 𝜓 → 𝜑 ) )
Proof
Step
Hyp
Ref
Expression
1
luklem3 ⊢ ( 𝜑 → ( ( ( ¬ 𝜑 → 𝜑 ) → 𝜑 ) → ( 𝜓 → 𝜑 ) ) )
2
luklem4 ⊢ ( ( ( ( ¬ 𝜑 → 𝜑 ) → 𝜑 ) → ( 𝜓 → 𝜑 ) ) → ( 𝜓 → 𝜑 ) )
3
1 2
luklem1 ⊢ ( 𝜑 → ( 𝜓 → 𝜑 ) )