This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mpd3an3

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

Ref Expression
Hypotheses mpd3an3.2 ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜒 )
mpd3an3.3 ⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) → 𝜃 )
Assertion mpd3an3 ( ( 𝜑 ∧ 𝜓 ) → 𝜃 )

Proof

Step Hyp Ref Expression
1 mpd3an3.2 ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜒 )
2 mpd3an3.3 ⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) → 𝜃 )
3 2 3expa ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) → 𝜃 )
4 1 3 mpdan ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜃 )