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  8036  omlimcl  8499  odi  8500  oelim2  8516  mapxpen  9063  unwdomg  9477  dfac12lem2  10043  infunsdom  10111  fin1a2s  10312  ccatpfx  14610  frlmup1  21737  fbasrn  23800  lmmbr  25186  grporcan  30500  unoplin  31902  hmoplin  31924  superpos  32336  ccatf1  32937  subfacp1lem5  35249  matunitlindflem1  37676  poimirlem4  37684  itg2addnclem  37731  ftc1anclem6  37758  fdc  37805  ismtyres  37868  isdrngo2  38018  rngohomco  38034  rngoisocnv  38041  dssmapnvod  44137  climxrrelem  45871  dvdsn1add  46061  dvnprodlem1  46068  stoweidlem27  46149  fourierdlem97  46325  qndenserrnbllem  46416  sge0iunmptlemfi  46535