Metamath Proof Explorer

Theorem merlem8

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

		Ref	Expression
	Assertion	merlem8	\|- ( ( ( ps -> ch ) -> th ) -> ( ( ( ch -> ta ) -> ( -. th -> -. ps ) ) -> th ) )

Proof

Step	Hyp	Ref	Expression
1		meredith	\|- ( ( ( ( ( ph -> ph ) -> ( -. ph -> -. ph ) ) -> ph ) -> ph ) -> ( ( ph -> ph ) -> ( ph -> ph ) ) )
2		merlem7	\|- ( ( ( ( ( ( ph -> ph ) -> ( -. ph -> -. ph ) ) -> ph ) -> ph ) -> ( ( ph -> ph ) -> ( ph -> ph ) ) ) -> ( ( ( ps -> ch ) -> th ) -> ( ( ( ch -> ta ) -> ( -. th -> -. ps ) ) -> th ) ) )
3	1 2	ax-mp	\|- ( ( ( ps -> ch ) -> th ) -> ( ( ( ch -> ta ) -> ( -. th -> -. ps ) ) -> th ) )

Step

Hyp

Ref

Expression

meredith

 |-  ( ( ( ( ( ph -> ph ) -> ( -. ph -> -. ph ) ) -> ph ) -> ph ) -> ( ( ph -> ph ) -> ( ph -> ph ) ) )

merlem7

 |-  ( ( ( ( ( ( ph -> ph ) -> ( -. ph -> -. ph ) ) -> ph ) -> ph ) -> ( ( ph -> ph ) -> ( ph -> ph ) ) ) -> ( ( ( ps -> ch ) -> th ) -> ( ( ( ch -> ta ) -> ( -. th -> -. ps ) ) -> th ) ) )

1 2

ax-mp

 |-  ( ( ( ps -> ch ) -> th ) -> ( ( ( ch -> ta ) -> ( -. th -> -. ps ) ) -> th ) )