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  8042  omlimcl  8505  odi  8506  oelim2  8523  mapxpen  9071  unwdomg  9489  dfac12lem2  10055  infunsdom  10123  fin1a2s  10324  ccatpfx  14624  frlmup1  21753  fbasrn  23828  lmmbr  25214  grporcan  30593  unoplin  31995  hmoplin  32017  superpos  32429  ccatf1  33031  subfacp1lem5  35378  matunitlindflem1  37813  poimirlem4  37821  itg2addnclem  37868  ftc1anclem6  37895  fdc  37942  ismtyres  38005  isdrngo2  38155  rngohomco  38171  rngoisocnv  38178  dssmapnvod  44257  climxrrelem  45989  dvdsn1add  46179  dvnprodlem1  46186  stoweidlem27  46267  fourierdlem97  46443  qndenserrnbllem  46534  sge0iunmptlemfi  46653