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

Metamath Proof Explorer

Theorem mp4an

Description: An inference based on modus ponens. (Contributed by Jeff Madsen, 15-Jun-2010)

Ref Expression
Hypotheses mp4an.1 ⊢ φ
mp4an.2 ⊢ ψ
mp4an.3 ⊢ χ
mp4an.4 ⊢ θ
mp4an.5 ⊢ φ ∧ ψ ∧ χ ∧ θ → τ
Assertion mp4an ⊢ τ

Proof

Step Hyp Ref Expression
1 mp4an.1 ⊢ φ
2 mp4an.2 ⊢ ψ
3 mp4an.3 ⊢ χ
4 mp4an.4 ⊢ θ
5 mp4an.5 ⊢ φ ∧ ψ ∧ χ ∧ θ → τ
6 1 2 pm3.2i ⊢ φ ∧ ψ
7 3 4 pm3.2i ⊢ χ ∧ θ
8 6 7 5 mp2an ⊢ τ