Metamath Proof Explorer


Theorem merlem4

Description: Step 8 of Meredith's proof of Lukasiewicz axioms from his sole axiom. (Contributed by NM, 14-Dec-2002) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion merlem4 ( 𝜏 → ( ( 𝜏𝜑 ) → ( 𝜃𝜑 ) ) )

Proof

Step Hyp Ref Expression
1 meredith ( ( ( ( ( 𝜑𝜑 ) → ( ¬ 𝜃 → ¬ 𝜃 ) ) → 𝜃 ) → 𝜏 ) → ( ( 𝜏𝜑 ) → ( 𝜃𝜑 ) ) )
2 merlem3 ( ( ( ( ( ( 𝜑𝜑 ) → ( ¬ 𝜃 → ¬ 𝜃 ) ) → 𝜃 ) → 𝜏 ) → ( ( 𝜏𝜑 ) → ( 𝜃𝜑 ) ) ) → ( 𝜏 → ( ( 𝜏𝜑 ) → ( 𝜃𝜑 ) ) ) )
3 1 2 ax-mp ( 𝜏 → ( ( 𝜏𝜑 ) → ( 𝜃𝜑 ) ) )