Theorem adantlrl 751

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 475	. 2 ⊢ ((𝜏 ∧ 𝜓) → 𝜓)
2		adantl2.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylanl2 680	1 ⊢ (((𝜑 ∧ (𝜏 ∧ 𝜓)) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 382

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 195  df-an 384

This theorem is referenced by:  omlimcl  7518  odi  7519  oelim2  7535  mapxpen  7984  unwdomg  8345  dfac12lem2  8822  infunsdom  8892  fin1a2s  9092  frlmup1  19894  fbasrn  21436  lmmbr  22778  grporcan  26518  unoplin  27965  hmoplin  27987  superpos  28399  subfacp1lem5  30222  matunitlindflem1  32374  poimirlem4  32382  itg2addnclem  32430  ftc1anclem6  32459  fdc  32510  ismtyres  32576  isdrngo2  32726  rngohomco  32742  rngoisocnv  32749  dssmapnvod  37133  dvdsn1add  38629  dvnprodlem1  38636  stoweidlem27  38720  fourierdlem97  38896  qndenserrnbllem  38990  sge0iunmptlemfi  39106