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 ⊢ 𝜏