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

Metamath Proof Explorer

Theorem mpsyl4anc

Description: An elimination deduction. (Contributed by Alan Sare, 17-Oct-2017)

Step	Hyp	Ref	Expression
1		mpsyl4anc.1	$⊢ φ$
2		mpsyl4anc.2	$⊢ ψ$
3		mpsyl4anc.3	$⊢ χ$
4		mpsyl4anc.4	$⊢ θ \to τ$
5		mpsyl4anc.5	$⊢ (((φ \land ψ) \land χ) \land τ) \to η$
6	1	a1i	$⊢ θ \to φ$
7	2	a1i	$⊢ θ \to ψ$
8	3	a1i	$⊢ θ \to χ$
9	6 7 8 4 5	syl1111anc	$⊢ θ \to η$