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

Metamath Proof Explorer

Theorem mp3and

Description: A deduction based on modus ponens. (Contributed by Mario Carneiro, 24-Dec-2016)

Ref Expression
Hypotheses mp3and.1 ⊢ ( 𝜑 → 𝜓 )
mp3and.2 ⊢ ( 𝜑 → 𝜒 )
mp3and.3 ⊢ ( 𝜑 → 𝜃 )
mp3and.4 ⊢ ( 𝜑 → ( ( 𝜓 ∧ 𝜒 ∧ 𝜃 ) → 𝜏 ) )
Assertion mp3and ( 𝜑 → 𝜏 )

Proof

Step Hyp Ref Expression
1 mp3and.1 ⊢ ( 𝜑 → 𝜓 )
2 mp3and.2 ⊢ ( 𝜑 → 𝜒 )
3 mp3and.3 ⊢ ( 𝜑 → 𝜃 )
4 mp3and.4 ⊢ ( 𝜑 → ( ( 𝜓 ∧ 𝜒 ∧ 𝜃 ) → 𝜏 ) )
5 1 2 3 3jca ⊢ ( 𝜑 → ( 𝜓 ∧ 𝜒 ∧ 𝜃 ) )
6 5 4 mpd ⊢ ( 𝜑 → 𝜏 )