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  8124  omlimcl  8615  odi  8616  oelim2  8632  mapxpen  9182  unwdomg  9622  dfac12lem2  10183  infunsdom  10251  fin1a2s  10452  ccatpfx  14736  frlmup1  21836  fbasrn  23908  lmmbr  25306  grporcan  30547  unoplin  31949  hmoplin  31971  superpos  32383  ccatf1  32918  subfacp1lem5  35169  matunitlindflem1  37603  poimirlem4  37611  itg2addnclem  37658  ftc1anclem6  37685  fdc  37732  ismtyres  37795  isdrngo2  37945  rngohomco  37961  rngoisocnv  37968  dssmapnvod  44010  climxrrelem  45705  dvdsn1add  45895  dvnprodlem1  45902  stoweidlem27  45983  fourierdlem97  46159  qndenserrnbllem  46250  sge0iunmptlemfi  46369