Theorem adantlrl 721

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 682	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  8052  omlimcl  8515  odi  8516  oelim2  8533  mapxpen  9083  unwdomg  9501  dfac12lem2  10067  infunsdom  10135  fin1a2s  10336  ccatpfx  14636  frlmup1  21765  fbasrn  23840  lmmbr  25226  grporcan  30605  unoplin  32007  hmoplin  32029  superpos  32441  ccatf1  33041  subfacp1lem5  35397  matunitlindflem1  37861  poimirlem4  37869  itg2addnclem  37916  ftc1anclem6  37943  fdc  37990  ismtyres  38053  isdrngo2  38203  rngohomco  38219  rngoisocnv  38226  dssmapnvod  44370  climxrrelem  46101  dvdsn1add  46291  dvnprodlem1  46298  stoweidlem27  46379  fourierdlem97  46555  qndenserrnbllem  46646  sge0iunmptlemfi  46765