Theorem adantlrr 729

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
adantlrr	⊢ (((𝜑 ∧ (𝜓 ∧ 𝜏)) ∧ 𝜒) → 𝜃)

Proof of Theorem adantlrr

Step	Hyp	Ref	Expression
1		simpl 485	. 2 ⊢ ((𝜓 ∧ 𝜏) → 𝜓)
2		adantl2.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylanl2 689	1 ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜏)) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  disjxiun  5087  2ndconst  8064  oelim  8487  odi  8532  marypha1lem  9365  dfac12lem2  10087  infunsdom  10155  isf34lem4  10320  distrlem1pr  10969  lcmgcdlem  16612  lcmdvds  16614  drsdirfi  18309  isacs3lem  18546  conjnmzb  19265  psgndif  21623  frlmsslsp  21817  metss2lem  24540  nghmcn  24774  bndth  24989  itg2monolem1  25781  dvmptfsum  26006  ply1divex  26166  itgulm  26437  rpvmasumlem  27517  dchrmusum2  27524  dchrisum0lem2  27548  dchrisum0lem3  27549  mulog2sumlem2  27565  pntibndlem3  27622  wwlksubclwwlk  30195  blocni  30943  superpos  32492  chirredlem2  32529  eulerpartlemgvv  34617  ballotlemfc0  34734  ballotlemfcc  34735  bj-finsumval0  37715  pibt2  37849  fin2solem  38043  matunitlindflem1  38053  poimirlem28  38085  heicant  38092  ftc1anclem6  38135  ftc1anc  38138  fdc  38182  incsequz  38185  ismtyres  38245  isdrngo2  38395  rngohomco  38411  keridl  38469  linepsubN  40314  pmapsub  40330  fsuppind  43110  mhpind  43114  mzpcompact2lem  43270  pellex  43350  monotuz  43456  unxpwdom3  43610  cantnfresb  43839  dssmapnvod  44534  radcnvrat  44828  fprodexp  46108  fprodabs2  46109  climxrrelem  46261  dvnprodlem1  46458  stoweidlem34  46546  fourierdlem42  46661  elaa2  46746  sge0iunmptlemfi  46925  aacllem  50360