Theorem adantlrl 699

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 471	. 2 ⊢ ((𝜏 ∧ 𝜓) → 𝜓)
2		adantl2.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylanl2 660	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 197  df-an 383

This theorem is referenced by:  omlimcl  7812  odi  7813  oelim2  7829  mapxpen  8282  unwdomg  8645  dfac12lem2  9168  infunsdom  9238  fin1a2s  9438  frlmup1  20354  fbasrn  21908  lmmbr  23275  grporcan  27712  unoplin  29119  hmoplin  29141  superpos  29553  subfacp1lem5  31504  matunitlindflem1  33738  poimirlem4  33746  itg2addnclem  33793  ftc1anclem6  33822  fdc  33873  ismtyres  33939  isdrngo2  34089  rngohomco  34105  rngoisocnv  34112  dssmapnvod  38840  climxrrelem  40499  dvdsn1add  40672  dvnprodlem1  40679  stoweidlem27  40761  fourierdlem97  40937  qndenserrnbllem  41031  sge0iunmptlemfi  41147