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

Metamath Proof Explorer

Theorem ad5ant2345

Description: Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017)

		Ref	Expression
	Hypothesis	ad5ant2345.1	$⊢ (((φ \land ψ) \land χ) \land θ) \to τ$
	Assertion	ad5ant2345	$⊢ ((((η \land φ) \land ψ) \land χ) \land θ) \to τ$

Step	Hyp	Ref	Expression
1		ad5ant2345.1	$⊢ (((φ \land ψ) \land χ) \land θ) \to τ$
2	1	exp41	$⊢ φ \to (ψ \to (χ \to (θ \to τ)))$
3	2	adantl	$⊢ (η \land φ) \to (ψ \to (χ \to (θ \to τ)))$
4	3	imp41	$⊢ ((((η \land φ) \land ψ) \land χ) \land θ) \to τ$