Metamath Proof Explorer


Theorem mp3anr3

Description: An inference based on modus ponens. (Contributed by NM, 19-Oct-2007)

Ref Expression
Hypotheses mp3anr3.1 𝜃
mp3anr3.2 ( ( 𝜑 ∧ ( 𝜓𝜒𝜃 ) ) → 𝜏 )
Assertion mp3anr3 ( ( 𝜑 ∧ ( 𝜓𝜒 ) ) → 𝜏 )

Proof

Step Hyp Ref Expression
1 mp3anr3.1 𝜃
2 mp3anr3.2 ( ( 𝜑 ∧ ( 𝜓𝜒𝜃 ) ) → 𝜏 )
3 2 ancoms ( ( ( 𝜓𝜒𝜃 ) ∧ 𝜑 ) → 𝜏 )
4 1 3 mp3anl3 ( ( ( 𝜓𝜒 ) ∧ 𝜑 ) → 𝜏 )
5 4 ancoms ( ( 𝜑 ∧ ( 𝜓𝜒 ) ) → 𝜏 )