Theorem adantllr 481

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)

Hypothesis

Ref	Expression
adantl2.1	⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
adantllr	⊢ ((((𝜑 ∧ 𝜏) ∧ 𝜓) ∧ 𝜒) → 𝜃)

Proof of Theorem adantllr

Step	Hyp	Ref	Expression
1		simpl 109	. 2 ⊢ ((𝜑 ∧ 𝜏) → 𝜑)
2		adantl2.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylanl1 402	1 ⊢ ((((𝜑 ∧ 𝜏) ∧ 𝜓) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  ad4ant13  513  ad4ant134  1220  ad5ant145  1247  r19.29an  2649  diffifi  7005  fimax2gtrilemstep  7011  cnegexlem3  8264  cnegex  8265  lemul12b  8949  climshftlemg  11683  prodeq2  11938  fprodmodd  12022  lcmdvds  12471  pw2dvdslemn  12557  dfgrp3mlem  13500  tgcl  14606  metss  15036  mpomulcn  15108  ivthinclemlr  15179  ivthinclemur  15181  nnnninfex  16094