Theorem adantlrl 719

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 680	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  8141  omlimcl  8634  odi  8635  oelim2  8651  mapxpen  9209  unwdomg  9653  dfac12lem2  10214  infunsdom  10282  fin1a2s  10483  ccatpfx  14749  frlmup1  21841  fbasrn  23913  lmmbr  25311  grporcan  30550  unoplin  31952  hmoplin  31974  superpos  32386  ccatf1  32915  subfacp1lem5  35152  matunitlindflem1  37576  poimirlem4  37584  itg2addnclem  37631  ftc1anclem6  37658  fdc  37705  ismtyres  37768  isdrngo2  37918  rngohomco  37934  rngoisocnv  37941  dssmapnvod  43982  climxrrelem  45670  dvdsn1add  45860  dvnprodlem1  45867  stoweidlem27  45948  fourierdlem97  46124  qndenserrnbllem  46215  sge0iunmptlemfi  46334