Theorem adantl3r

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

	Ref	Expression
Hypothesis	adantl3r.1	⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) ∧ 𝜃 ) → 𝜏 )
Assertion	adantl3r	⊢ ( ( ( ( ( 𝜑 ∧ 𝜂 ) ∧ 𝜓 ) ∧ 𝜒 ) ∧ 𝜃 ) → 𝜏 )

Proof

Step	Hyp	Ref	Expression
1		adantl3r.1	⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) ∧ 𝜃 ) → 𝜏 )
2		id	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝜑 ∧ 𝜓 ) )
3	2	adantlr	⊢ ( ( ( 𝜑 ∧ 𝜂 ) ∧ 𝜓 ) → ( 𝜑 ∧ 𝜓 ) )
4	3 1	sylanl1	⊢ ( ( ( ( ( 𝜑 ∧ 𝜂 ) ∧ 𝜓 ) ∧ 𝜒 ) ∧ 𝜃 ) → 𝜏 )