Theorem adantlrr 722

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  disjxiun  5083  2ndconst  8044  oelim  8462  odi  8507  marypha1lem  9339  dfac12lem2  10058  infunsdom  10126  isf34lem4  10290  distrlem1pr  10939  lcmgcdlem  16566  lcmdvds  16568  drsdirfi  18262  isacs3lem  18499  conjnmzb  19219  psgndif  21592  frlmsslsp  21786  metss2lem  24486  nghmcn  24720  bndth  24935  itg2monolem1  25727  dvmptfsum  25952  ply1divex  26112  itgulm  26386  rpvmasumlem  27464  dchrmusum2  27471  dchrisum0lem2  27495  dchrisum0lem3  27496  mulog2sumlem2  27512  pntibndlem3  27569  wwlksubclwwlk  30143  blocni  30891  superpos  32440  chirredlem2  32477  eulerpartlemgvv  34536  ballotlemfc0  34653  ballotlemfcc  34654  bj-finsumval0  37615  pibt2  37747  fin2solem  37941  matunitlindflem1  37951  poimirlem28  37983  heicant  37990  ftc1anclem6  38033  ftc1anc  38036  fdc  38080  incsequz  38083  ismtyres  38143  isdrngo2  38293  rngohomco  38309  keridl  38367  linepsubN  40212  pmapsub  40228  fsuppind  43037  mhpind  43041  mzpcompact2lem  43197  pellex  43281  monotuz  43387  unxpwdom3  43541  cantnfresb  43770  dssmapnvod  44465  radcnvrat  44759  fprodexp  46042  fprodabs2  46043  climxrrelem  46195  dvnprodlem1  46392  stoweidlem34  46480  fourierdlem42  46595  elaa2  46680  sge0iunmptlemfi  46859  aacllem  50288