Theorem adantlrl 720

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
adantlrl	⊢ (((𝜑 ∧ (𝜏 ∧ 𝜓)) ∧ 𝜒) → 𝜃)

Proof of Theorem adantlrl

Step	Hyp	Ref	Expression
1		simpr 484	. 2 ⊢ ((𝜏 ∧ 𝜓) → 𝜓)
2		adantl2.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylanl2 681	1 ⊢ (((𝜑 ∧ (𝜏 ∧ 𝜓)) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396

This theorem is referenced by:  1stconst  8040  omlimcl  8503  odi  8504  oelim2  8520  mapxpen  9067  unwdomg  9495  dfac12lem2  10058  infunsdom  10126  fin1a2s  10327  ccatpfx  14625  frlmup1  21723  fbasrn  23787  lmmbr  25174  grporcan  30480  unoplin  31882  hmoplin  31904  superpos  32316  ccatf1  32903  subfacp1lem5  35156  matunitlindflem1  37595  poimirlem4  37603  itg2addnclem  37650  ftc1anclem6  37677  fdc  37724  ismtyres  37787  isdrngo2  37937  rngohomco  37953  rngoisocnv  37960  dssmapnvod  43993  climxrrelem  45731  dvdsn1add  45921  dvnprodlem1  45928  stoweidlem27  46009  fourierdlem97  46185  qndenserrnbllem  46276  sge0iunmptlemfi  46395