Theorem adantlrl 719

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

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  1stconst  8086  omlimcl  8578  odi  8579  oelim2  8595  mapxpen  9143  unwdomg  9579  dfac12lem2  10139  infunsdom  10209  fin1a2s  10409  ccatpfx  14651  frlmup1  21353  fbasrn  23388  lmmbr  24775  grporcan  29771  unoplin  31173  hmoplin  31195  superpos  31607  ccatf1  32115  subfacp1lem5  34175  matunitlindflem1  36484  poimirlem4  36492  itg2addnclem  36539  ftc1anclem6  36566  fdc  36613  ismtyres  36676  isdrngo2  36826  rngohomco  36842  rngoisocnv  36849  dssmapnvod  42771  climxrrelem  44465  dvdsn1add  44655  dvnprodlem1  44662  stoweidlem27  44743  fourierdlem97  44919  qndenserrnbllem  45010  sge0iunmptlemfi  45129