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  8125  omlimcl  8616  odi  8617  oelim2  8633  mapxpen  9183  unwdomg  9624  dfac12lem2  10185  infunsdom  10253  fin1a2s  10454  ccatpfx  14739  frlmup1  21818  fbasrn  23892  lmmbr  25292  grporcan  30537  unoplin  31939  hmoplin  31961  superpos  32373  ccatf1  32933  subfacp1lem5  35189  matunitlindflem1  37623  poimirlem4  37631  itg2addnclem  37678  ftc1anclem6  37705  fdc  37752  ismtyres  37815  isdrngo2  37965  rngohomco  37981  rngoisocnv  37988  dssmapnvod  44033  climxrrelem  45764  dvdsn1add  45954  dvnprodlem1  45961  stoweidlem27  46042  fourierdlem97  46218  qndenserrnbllem  46309  sge0iunmptlemfi  46428