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

Metamath Proof Explorer

Theorem mp3an3an

Description: mp3an with antecedents in standard conjunction form and with two hypotheses which are implications. (Contributed by Alan Sare, 28-Aug-2016)

	Ref	Expression
Hypotheses	mp3an3an.1	$⊢ φ$
	mp3an3an.2	$⊢ ψ \to χ$
	mp3an3an.3	$⊢ θ \to τ$
	mp3an3an.4	$⊢ (φ \land χ \land τ) \to η$
Assertion	mp3an3an	$⊢ (ψ \land θ) \to η$

Proof

Step	Hyp	Ref	Expression
1		mp3an3an.1	$⊢ φ$
2		mp3an3an.2	$⊢ ψ \to χ$
3		mp3an3an.3	$⊢ θ \to τ$
4		mp3an3an.4	$⊢ (φ \land χ \land τ) \to η$
5	1 4	mp3an1	$⊢ (χ \land τ) \to η$
6	2 3 5	syl2an	$⊢ (ψ \land θ) \to η$