Theorem adantlrr 731

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

Syntax hints:   → wi 4   ∧ wa 399

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 400

This theorem is referenced by:  disjxiun  5096  2ndconst  8075  oelim  8498  odi  8543  marypha1lem  9376  dfac12lem2  10098  infunsdom  10166  isf34lem4  10331  distrlem1pr  10980  lcmgcdlem  16623  lcmdvds  16625  drsdirfi  18320  isacs3lem  18557  conjnmzb  19276  psgndif  21634  frlmsslsp  21828  metss2lem  24551  nghmcn  24785  bndth  25000  itg2monolem1  25792  dvmptfsum  26017  ply1divex  26177  itgulm  26448  rpvmasumlem  27528  dchrmusum2  27535  dchrisum0lem2  27559  dchrisum0lem3  27560  mulog2sumlem2  27576  pntibndlem3  27633  wwlksubclwwlk  30206  blocni  30954  superpos  32503  chirredlem2  32540  eulerpartlemgvv  34634  ballotlemfc0  34751  ballotlemfcc  34752  bj-finsumval0  37741  pibt2  37875  fin2solem  38069  matunitlindflem1  38079  poimirlem28  38111  heicant  38118  ftc1anclem6  38161  ftc1anc  38164  fdc  38208  incsequz  38211  ismtyres  38271  isdrngo2  38421  rngohomco  38437  keridl  38495  linepsubN  40340  pmapsub  40356  fsuppind  43136  mhpind  43140  mzpcompact2lem  43296  pellex  43376  monotuz  43482  unxpwdom3  43636  cantnfresb  43865  dssmapnvod  44560  radcnvrat  44854  fprodexp  46134  fprodabs2  46135  climxrrelem  46287  dvnprodlem1  46484  stoweidlem34  46572  fourierdlem42  46687  elaa2  46772  sge0iunmptlemfi  46951  aacllem  50386