Theorem adantlrl 717

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 485	. 2 ⊢ ((𝜏 ∧ 𝜓) → 𝜓)
2		adantl2.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylanl2 678	1 ⊢ (((𝜑 ∧ (𝜏 ∧ 𝜓)) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  1stconst  7940  omlimcl  8409  odi  8410  oelim2  8426  mapxpen  8930  unwdomg  9343  dfac12lem2  9900  infunsdom  9970  fin1a2s  10170  ccatpfx  14414  frlmup1  21005  fbasrn  23035  lmmbr  24422  grporcan  28880  unoplin  30282  hmoplin  30304  superpos  30716  ccatf1  31223  subfacp1lem5  33146  matunitlindflem1  35773  poimirlem4  35781  itg2addnclem  35828  ftc1anclem6  35855  fdc  35903  ismtyres  35966  isdrngo2  36116  rngohomco  36132  rngoisocnv  36139  dssmapnvod  41628  climxrrelem  43290  dvdsn1add  43480  dvnprodlem1  43487  stoweidlem27  43568  fourierdlem97  43744  qndenserrnbllem  43835  sge0iunmptlemfi  43951