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  8099  omlimcl  8590  odi  8591  oelim2  8607  mapxpen  9157  unwdomg  9598  dfac12lem2  10159  infunsdom  10227  fin1a2s  10428  ccatpfx  14719  frlmup1  21758  fbasrn  23822  lmmbr  25210  grporcan  30499  unoplin  31901  hmoplin  31923  superpos  32335  ccatf1  32924  subfacp1lem5  35206  matunitlindflem1  37640  poimirlem4  37648  itg2addnclem  37695  ftc1anclem6  37722  fdc  37769  ismtyres  37832  isdrngo2  37982  rngohomco  37998  rngoisocnv  38005  dssmapnvod  44044  climxrrelem  45778  dvdsn1add  45968  dvnprodlem1  45975  stoweidlem27  46056  fourierdlem97  46232  qndenserrnbllem  46323  sge0iunmptlemfi  46442