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

Metamath Proof Explorer

Theorem adantl4r

Description: Deduction adding 1 conjunct to antecedent. (Contributed by Thierry Arnoux, 11-Feb-2018)

		Ref	Expression
	Hypothesis	adantl4r.1	$⊢ ((((φ \land σ) \land ρ) \land μ) \land λ) \to κ$
	Assertion	adantl4r	$⊢ (((((φ \land ζ) \land σ) \land ρ) \land μ) \land λ) \to κ$

Step	Hyp	Ref	Expression
1		adantl4r.1	$⊢ ((((φ \land σ) \land ρ) \land μ) \land λ) \to κ$
2	1	ex	$⊢ (((φ \land σ) \land ρ) \land μ) \to (λ \to κ)$
3	2	adantl3r	$⊢ ((((φ \land ζ) \land σ) \land ρ) \land μ) \to (λ \to κ)$
4	3	imp	$⊢ (((((φ \land ζ) \land σ) \land ρ) \land μ) \land λ) \to κ$