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

Syntax hints:   → wi 4   ∧ wa 399

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 400

This theorem is referenced by:  1stconst  7846  omlimcl  8284  odi  8285  oelim2  8301  mapxpen  8790  unwdomg  9178  dfac12lem2  9723  infunsdom  9793  fin1a2s  9993  ccatpfx  14231  frlmup1  20714  fbasrn  22735  lmmbr  24109  grporcan  28553  unoplin  29955  hmoplin  29977  superpos  30389  ccatf1  30897  subfacp1lem5  32813  matunitlindflem1  35459  poimirlem4  35467  itg2addnclem  35514  ftc1anclem6  35541  fdc  35589  ismtyres  35652  isdrngo2  35802  rngohomco  35818  rngoisocnv  35825  dssmapnvod  41246  climxrrelem  42908  dvdsn1add  43098  dvnprodlem1  43105  stoweidlem27  43186  fourierdlem97  43362  qndenserrnbllem  43453  sge0iunmptlemfi  43569