Theorem adantlrl 716

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

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  1stconst  8088  omlimcl  8580  odi  8581  oelim2  8597  mapxpen  9145  unwdomg  9581  dfac12lem2  10141  infunsdom  10211  fin1a2s  10411  ccatpfx  14655  frlmup1  21572  fbasrn  23608  lmmbr  25006  grporcan  30038  unoplin  31440  hmoplin  31462  superpos  31874  ccatf1  32382  subfacp1lem5  34473  matunitlindflem1  36787  poimirlem4  36795  itg2addnclem  36842  ftc1anclem6  36869  fdc  36916  ismtyres  36979  isdrngo2  37129  rngohomco  37145  rngoisocnv  37152  dssmapnvod  43073  climxrrelem  44763  dvdsn1add  44953  dvnprodlem1  44960  stoweidlem27  45041  fourierdlem97  45217  qndenserrnbllem  45308  sge0iunmptlemfi  45427