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 484	. 2 ⊢ ((𝜏 ∧ 𝜓) → 𝜓)
2		adantl2.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylanl2 681	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  8082  omlimcl  8545  odi  8546  oelim2  8562  mapxpen  9113  unwdomg  9544  dfac12lem2  10105  infunsdom  10173  fin1a2s  10374  ccatpfx  14673  frlmup1  21714  fbasrn  23778  lmmbr  25165  grporcan  30454  unoplin  31856  hmoplin  31878  superpos  32290  ccatf1  32877  subfacp1lem5  35178  matunitlindflem1  37617  poimirlem4  37625  itg2addnclem  37672  ftc1anclem6  37699  fdc  37746  ismtyres  37809  isdrngo2  37959  rngohomco  37975  rngoisocnv  37982  dssmapnvod  44016  climxrrelem  45754  dvdsn1add  45944  dvnprodlem1  45951  stoweidlem27  46032  fourierdlem97  46208  qndenserrnbllem  46299  sge0iunmptlemfi  46418