Theorem adantlrl 752

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

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  omlimcl  7545  odi  7546  oelim2  7562  mapxpen  8011  unwdomg  8372  dfac12lem2  8849  infunsdom  8919  fin1a2s  9119  frlmup1  19956  fbasrn  21498  lmmbr  22864  grporcan  26756  unoplin  28163  hmoplin  28185  superpos  28597  subfacp1lem5  30420  matunitlindflem1  32575  poimirlem4  32583  itg2addnclem  32631  ftc1anclem6  32660  fdc  32711  ismtyres  32777  isdrngo2  32927  rngohomco  32943  rngoisocnv  32950  dssmapnvod  37334  dvdsn1add  38829  dvnprodlem1  38836  stoweidlem27  38920  fourierdlem97  39096  qndenserrnbllem  39190  sge0iunmptlemfi  39306