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  8050  omlimcl  8513  odi  8514  oelim2  8531  mapxpen  9081  unwdomg  9499  dfac12lem2  10067  infunsdom  10135  fin1a2s  10336  ccatpfx  14663  frlmup1  21778  fbasrn  23849  lmmbr  25225  grporcan  30589  unoplin  31991  hmoplin  32013  superpos  32425  ccatf1  33009  subfacp1lem5  35366  matunitlindflem1  37937  poimirlem4  37945  itg2addnclem  37992  ftc1anclem6  38019  fdc  38066  ismtyres  38129  isdrngo2  38279  rngohomco  38295  rngoisocnv  38302  dssmapnvod  44447  climxrrelem  46177  dvdsn1add  46367  dvnprodlem1  46374  stoweidlem27  46455  fourierdlem97  46631  qndenserrnbllem  46722  sge0iunmptlemfi  46841