Theorem adantlrl 732

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  1stconst  8083  omlimcl  8551  odi  8552  oelim2  8569  mapxpen  9119  unwdomg  9534  dfac12lem2  10116  infunsdom  10184  fin1a2s  10386  ccatpfx  14728  frlmup1  21908  fbasrn  24002  lmmbr  25378  grporcan  30779  unoplin  32181  hmoplin  32203  superpos  32615  ccatf1  33182  subfacp1lem5  35547  matunitlindflem1  38127  poimirlem4  38135  itg2addnclem  38182  ftc1anclem6  38209  fdc  38256  ismtyres  38319  isdrngo2  38469  rngohomco  38485  rngoisocnv  38492  dssmapnvod  44608  climxrrelem  46321  dvdsn1add  46511  dvnprodlem1  46518  stoweidlem27  46599  fourierdlem97  46775  qndenserrnbllem  46866  sge0iunmptlemfi  46985