Metamath Proof Explorer


Theorem mp2

Description: A double modus ponens inference. (Contributed by NM, 5-Apr-1994)

Ref Expression
Hypotheses mp2.1 𝜑
mp2.2 𝜓
mp2.3 ( 𝜑 → ( 𝜓𝜒 ) )
Assertion mp2 𝜒

Proof

Step Hyp Ref Expression
1 mp2.1 𝜑
2 mp2.2 𝜓
3 mp2.3 ( 𝜑 → ( 𝜓𝜒 ) )
4 1 3 ax-mp ( 𝜓𝜒 )
5 2 4 ax-mp 𝜒