Theorem adantlrl 726

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  1stconst  8046  omlimcl  8510  odi  8511  oelim2  8528  mapxpen  9078  unwdomg  9496  dfac12lem2  10065  infunsdom  10133  fin1a2s  10334  ccatpfx  14661  frlmup1  21780  fbasrn  23874  lmmbr  25250  grporcan  30614  unoplin  32016  hmoplin  32038  superpos  32450  ccatf1  33035  subfacp1lem5  35419  matunitlindflem1  37990  poimirlem4  37998  itg2addnclem  38045  ftc1anclem6  38072  fdc  38119  ismtyres  38182  isdrngo2  38332  rngohomco  38348  rngoisocnv  38355  dssmapnvod  44471  climxrrelem  46199  dvdsn1add  46389  dvnprodlem1  46396  stoweidlem27  46477  fourierdlem97  46653  qndenserrnbllem  46744  sge0iunmptlemfi  46863