Theorem adantlrl 730

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  1stconst  8074  omlimcl  8542  odi  8543  oelim2  8560  mapxpen  9111  unwdomg  9529  dfac12lem2  10098  infunsdom  10166  fin1a2s  10368  ccatpfx  14711  frlmup1  21830  fbasrn  23924  lmmbr  25300  grporcan  30667  unoplin  32069  hmoplin  32091  superpos  32503  ccatf1  33088  subfacp1lem5  35498  matunitlindflem1  38079  poimirlem4  38087  itg2addnclem  38134  ftc1anclem6  38161  fdc  38208  ismtyres  38271  isdrngo2  38421  rngohomco  38437  rngoisocnv  38444  dssmapnvod  44560  climxrrelem  46287  dvdsn1add  46477  dvnprodlem1  46484  stoweidlem27  46565  fourierdlem97  46741  qndenserrnbllem  46832  sge0iunmptlemfi  46951