Theorem wl-impchain-mp-0 35525

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 5, 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.)

Hypotheses

Ref	Expression
wl-impchain-mp-0.a	⊢ 𝜓
wl-impchain-mp-0.b	⊢ (𝜓 → 𝜑)

Assertion

Ref	Expression
wl-impchain-mp-0	⊢ 𝜑

Proof of Theorem wl-impchain-mp-0

Step	Hyp	Ref	Expression
1		wl-impchain-mp-0.a	. 2 ⊢ 𝜓
2		wl-impchain-mp-0.b	. 2 ⊢ (𝜓 → 𝜑)
3	1, 2	ax-mp 5	1 ⊢ 𝜑

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5

This theorem is referenced by:  wl-impchain-mp-1  35526  wl-impchain-com-1.2  35530