Theorem wl-impchain-mp-0

Description: This theorem is the start of a proof recursion scheme where we replace the consequent of an implication chain. The number '0' in the theorem name indicates that the modified chain has no antecedents.

This theorem is in fact a copy of ax-mp , and is repeated here to emphasize the recursion using similar theorem names. (Contributed by Wolf Lammen, 6-Jul-2019) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	wl-impchain-mp-0.a	|- ps
	wl-impchain-mp-0.b	|- ( ps -> ph )
Assertion	wl-impchain-mp-0	|- ph

Proof

Step	Hyp	Ref	Expression
1		wl-impchain-mp-0.a	|- ps
2		wl-impchain-mp-0.b	|- ( ps -> ph )
3	1 2	ax-mp	|- ph