Theorem adantlrl 733

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  1stconst  8101  omlimcl  8569  odi  8570  oelim2  8587  mapxpen  9145  unwdomg  9560  dfac12lem2  10151  infunsdom  10219  fin1a2s  10420  ccatf1  14660  ccatpfx  14774  frlmup1  22017  matunitlindflem1  22907  fbasrn  24116  lmmbr  25492  grporcan  31007  unoplin  32409  hmoplin  32431  superpos  32843  subfacp1lem5  35771  poimirlem4  38381  itg2addnclem  38428  ftc1anclem6  38455  fdc  38503  ismtyres  38566  isdrngo2  38716  rngohomco  38732  rngoisocnv  38739  dssmapnvod  44868  climxrrelem  46585  dvdsn1add  46775  dvnprodlem1  46782  stoweidlem27  46863  fourierdlem97  47039  qndenserrnbllem  47130  sge0iunmptlemfi  47249