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  8079  omlimcl  8542  odi  8543  oelim2  8559  mapxpen  9107  unwdomg  9537  dfac12lem2  10098  infunsdom  10166  fin1a2s  10367  ccatpfx  14666  frlmup1  21707  fbasrn  23771  lmmbr  25158  grporcan  30447  unoplin  31849  hmoplin  31871  superpos  32283  ccatf1  32870  subfacp1lem5  35171  matunitlindflem1  37610  poimirlem4  37618  itg2addnclem  37665  ftc1anclem6  37692  fdc  37739  ismtyres  37802  isdrngo2  37952  rngohomco  37968  rngoisocnv  37975  dssmapnvod  44009  climxrrelem  45747  dvdsn1add  45937  dvnprodlem1  45944  stoweidlem27  46025  fourierdlem97  46201  qndenserrnbllem  46292  sge0iunmptlemfi  46411