Theorem adantlrl 721

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 682	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  8043  omlimcl  8506  odi  8507  oelim2  8524  mapxpen  9074  unwdomg  9492  dfac12lem2  10058  infunsdom  10126  fin1a2s  10327  ccatpfx  14654  frlmup1  21788  fbasrn  23859  lmmbr  25235  grporcan  30604  unoplin  32006  hmoplin  32028  superpos  32440  ccatf1  33024  subfacp1lem5  35382  matunitlindflem1  37951  poimirlem4  37959  itg2addnclem  38006  ftc1anclem6  38033  fdc  38080  ismtyres  38143  isdrngo2  38293  rngohomco  38309  rngoisocnv  38316  dssmapnvod  44465  climxrrelem  46195  dvdsn1add  46385  dvnprodlem1  46392  stoweidlem27  46473  fourierdlem97  46649  qndenserrnbllem  46740  sge0iunmptlemfi  46859