Theorem syl21anc 837

Description: Syllogism combined with contraction. (Contributed by Jeff Hankins, 1-Aug-2009.)

Hypotheses

Ref	Expression
syl12anc.1	⊢ (𝜑 → 𝜓)
syl12anc.2	⊢ (𝜑 → 𝜒)
syl12anc.3	⊢ (𝜑 → 𝜃)
syl21anc.4	⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)

Assertion

Ref	Expression
syl21anc	⊢ (𝜑 → 𝜏)

Proof of Theorem syl21anc

Step	Hyp	Ref	Expression
1		syl12anc.1	. . 3 ⊢ (𝜑 → 𝜓)
2		syl12anc.2	. . 3 ⊢ (𝜑 → 𝜒)
3	1, 2	jca 513	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
4		syl12anc.3	. 2 ⊢ (𝜑 → 𝜃)
5		syl21anc.4	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)
6	3, 4, 5	syl2anc 585	1 ⊢ (𝜑 → 𝜏)

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  syl1111anc  839  rspc2dv  3626  wereu2  5673  frpomin  6339  funtpg  6601  funcnvtp  6609  funcnvqp  6610  fnund  6662  fun2d  6753  fvun1  6980  iinpreima  7068  ftpg  7151  fsnunf  7180  f1prex  7279  soisores  7321  isotr  7330  off  7685  caofrss  7703  caonncan  7708  fvmpocurryd  8253  oaf1o  8560  omeulem1  8579  oeordi  8584  oelimcl  8597  oeeulem  8598  oeeui  8599  oaabs2  8645  omabs  8647  coflton  8667  pmresg  8861  ralxpmap  8887  domunsncan  9069  sucdom2OLD  9079  sucdom2  9203  unxpdom2  9251  sucxpdom  9252  unblem4  9295  fodomfi  9322  hartogslem1  9534  cantnflt  9664  cantnflem3  9683  cantnflem4  9684  cnfcomlem  9691  cnfcom  9692  ttrcltr  9708  infxpenlem  10005  infxpenc  10010  fseqenlem1  10016  pwsdompw  10196  cfeq0  10248  cofsmo  10261  cfsmolem  10262  ssfin4  10302  hsmexlem4  10421  hsmexlem5  10422  axdc3lem2  10443  fpwwe2  10635  wunpr  10701  mulclpi  10885  mulcanenq  10952  distrlem4pr  11018  prlem934  11025  prlem936  11039  divge0d  13053  elfznelfzob  13735  seqcaopr2  14001  facavg  14258  swrdwrdsymb  14609  cats1un  14668  f1oun2prg  14865  sqrtdiv  15209  sqrtdivd  15367  mulcn2  15537  o1of2  15554  fsumsplit  15684  sumsplit  15711  isumless  15788  demoivreALT  16141  rpnnen2lem11  16164  gcdnncl  16445  qredeu  16592  rpdvds  16594  isprm5  16641  rpexp  16656  divnumden  16681  divdenle  16682  phimullem  16709  phisum  16720  pythagtriplem4  16749  pythagtriplem8  16753  pythagtriplem9  16754  pcgcd1  16807  sumhash  16826  fldivp1  16827  pockthlem  16835  setsfun  17101  setsfun0  17102  ssc2  17766  estrreslem1  18085  estrreslem1OLD  18086  tleile  18371  sgrppropd  18619  mndpropd  18647  grpidssd  18896  grpinvssd  18897  issubg2  19016  isnsg3  19035  eqgid  19055  gass  19160  symgextres  19288  gsmsymgreqlem2  19294  sylow1lem5  19465  sylow2alem2  19481  sylow3lem3  19492  efgredlemd  19607  efgredlem  19610  frgpnabllem1  19736  frgpnabllem2  19737  subgdmdprd  19899  ablfacrplem  19930  rglcom4d  20028  kerf1ghm  20275  issrngd  20462  lmodprop2d  20527  lsspropd  20621  pwssplit1  20663  lspvadd  20700  znidomb  21109  znrrg  21113  lindfind  21363  lindsind  21364  mplsubglem  21550  mplind  21623  mat1ghm  21977  mdetunilem1  22106  mdetunilem3  22108  mdetunilem4  22109  mdetunilem9  22114  cramerimplem2  22178  mat2pmatlin  22229  monmatcollpw  22273  cpmadugsumlemF  22370  mretopd  22588  neiptopnei  22628  neitr  22676  ufilen  23426  flimrest  23479  flimclslem  23480  fclsrest  23520  cnextcn  23563  haustsms2  23633  tsmsxplem2  23650  trust  23726  utoptop  23731  restutop  23734  ustuqtop4  23741  utopsnneiplem  23744  utop2nei  23747  utop3cls  23748  isucn2  23776  ucncn  23782  fmucnd  23789  trcfilu  23791  comet  24014  metustexhalf  24057  metustbl  24067  psmetutop  24068  nrmmetd  24075  reconnlem1  24334  reconnlem2  24335  fsumcn  24378  cmetcaulem  24797  iscmet3lem1  24800  iscmet3lem2  24801  bcthlem5  24837  cmslsschl  24886  rrxdstprj1  24918  minveclem4  24941  ovolfiniun  25010  itg1addlem4  25208  itg1addlem4OLD  25209  itg1addlem5  25210  itgsplitioo  25347  c1liplem1  25505  dvfsumlem1  25535  plyeq0lem  25716  quotcan  25814  psercnlem1  25929  cxplea  26196  birthdaylem3  26448  musumsum  26686  dvdsmulf1o  26688  dchrelbas4  26736  dchrhash  26764  gausslemma2dlem0d  26852  gausslemma2dlem1a  26858  2lgslem1a1  26882  2sqlem8a  26918  2sqlem8  26919  2sqcoprm  26928  2sqmod  26929  chto1ub  26969  vmadivsum  26975  dchrisumlem1  26982  dchrvmasumlem2  26991  dchrvmasumiflem1  26994  rpvmasum2  27005  mulog2sumlem2  27028  selberg2lem  27043  pntrmax  27057  pntpbnd1  27079  pntlemb  27090  pntlemj  27096  noextend  27159  cuteq0  27323  tgjustc1  27716  tgjustc2  27717  ercgrg  27758  motcgr  27777  tglineeltr  27872  colline  27890  miriso  27911  midexlem  27933  perpneq  27955  foot  27963  f1otrg  28112  axcontlem9  28220  uspgr1ewop  28495  nbupgrres  28611  structtocusgr  28693  wlkp1  28928  clwlkl1loop  29030  uspgrn2crct  29052  crctcshwlkn0lem5  29058  3trlond  29416  3pthond  29418  3spthond  29420  frgr3v  29518  vdgn1frgrv2  29539  numclwwlk3  29628  nmblolbii  30040  minvecolem3  30117  minvecolem4  30121  htthlem  30158  bcs2  30423  nmopub2tALT  31150  nmfnleub2  31167  eighmorth  31205  nmophmi  31272  nmopcoadji  31342  hstle  31471  atcvat3i  31637  opreu2reuALT  31705  iinabrex  31788  disjxpin  31807  fmptco1f1o  31845  off2  31854  xppreima2  31864  fgreu  31885  suppovss  31894  1stpreimas  31915  padct  31932  resf1o  31943  fpwrelmap  31946  xrofsup  31968  eliccelico  31976  elicoelioo  31977  iocinif  31980  difioo  31981  suppssnn0  32005  prmdvdsbc  32010  ccatf1  32103  pfxlsw2ccat  32104  wrdt2ind  32105  ressprs  32121  xrge0addgt0  32180  xrge0adddir  32181  gsumhashmul  32196  omndmul3  32219  gsumle  32230  symgcom  32232  pmtrcnel  32238  pmtrcnel2  32239  pmtrcnelor  32240  cycpmfv2  32261  trsp2cyc  32270  cycpmco2lem7  32279  cyc3genpm  32299  cycpmconjslem2  32302  cyc3conja  32304  archirng  32322  archirngz  32323  orngmul  32410  linds2eq  32486  nsgqusf1olem3  32515  ghmquskerlem1  32517  ghmqusker  32521  rhmpreimaidl  32526  lidlunitel  32530  unitpidl1  32531  elrspunidl  32535  drngidl  32540  isprmidlc  32555  qsidomlem1  32560  qsidomlem2  32561  qsnzr  32563  mxidlirredi  32576  mxidlirred  32577  qsdrngi  32598  qsdrnglem2  32599  ressply1evl  32636  deg1le0eq0  32644  ply1degltdimlem  32696  ply1degltdim  32697  lindsunlem  32698  lbsdiflsp0  32700  fedgmullem1  32703  fedgmullem2  32704  ply1annprmidl  32757  minplyirredlem  32758  irngnminplynz  32760  algextdeglem1  32761  1smat1  32773  madjusmdetlem2  32797  qtophaus  32805  locfinref  32810  zarclssn  32842  zar0ring  32847  zarmxt1  32849  rhmpreimacnlem  32853  rhmpreimacn  32854  metideq  32862  sqsscirc2  32878  tpr2rico  32881  fmcncfil  32900  lmxrge0  32921  lmdvg  32922  qqhval2lem  32950  qqhf  32955  qqhnm  32959  esumle  33045  gsumesum  33046  esumlef  33049  esumrnmpt2  33055  esumpcvgval  33065  esum2d  33080  ofcf  33090  ldsysgenld  33147  ldgenpisyslem1  33150  unelros  33158  difelros  33159  inelsros  33165  diffiunisros  33166  imambfm  33250  omssubadd  33288  inelcarsg  33299  carsgsigalem  33303  carsggect  33306  carsgclctunlem2  33307  oddpwdc  33342  eulerpartlems  33348  eulerpartlemb  33356  eulerpartlemt  33359  iwrdsplit  33375  sseqf  33380  sseqfres  33381  ballotlemfc0  33480  ballotlemfcc  33481  ballotlemfrcn0  33517  sgnsub  33532  plymulx0  33547  signsplypnf  33550  signsvtn0  33570  signstfvneq0  33572  signsvtp  33583  signsvtn  33584  fsum2dsub  33608  reprlt  33620  hashreprin  33621  reprgt  33622  reprpmtf1o  33627  chtvalz  33630  breprexplema  33631  breprexplemc  33633  breprexp  33634  circlemeth  33641  logdivsqrle  33651  hgt750lemb  33657  lpadlem3  33679  lpadleft  33684  bnj1536  33854  bnj1001  33959  bnj1280  34020  cvxsconn  34223  satffunlem1  34387  satffunlem2  34388  elmrsubrn  34500  neibastop3  35236  finxpsuclem  36267  poimirlem16  36493  poimirlem19  36496  poimirlem20  36497  poimirlem29  36506  mblfinlem3  36516  itg2addnclem3  36530  ftc1cnnclem  36548  lautlt  38951  lautcvr  38952  lauteq  38955  lautco  38957  ltrncl  38985  ltrncnvleN  38990  trljat2  39027  cdlemc6  39056  cdleme20c  39171  cdleme20j  39178  cdleme22e  39204  cdleme22eALTN  39205  cdlemg7aN  39485  cdlemg12e  39507  cdlemg17dALTN  39524  cdlemh  39677  cdlemkfid1N  39781  dibglbN  40026  diblss  40030  diclspsn  40054  dih1  40146  dihglbcpreN  40160  dihmeetlem4preN  40166  lcfrlem19  40421  aks4d1p8d1  40938  evlsvvval  41133  fsuppind  41160  mapfzcons  41440  mzpcl34  41455  mzpindd  41470  mzpsubst  41472  diophrw  41483  diophren  41537  irrapxlem1  41546  pellexlem5  41557  acongrep  41705  pwssplit4  41817  omlimcl2  41977  onexoegt  41979  oasubex  42022  omlim2  42035  nnoeomeqom  42048  nnawordexg  42063  succlg  42064  oacl2g  42066  onmcl  42067  omabs2  42068  omcl2  42069  tfsconcatrev  42084  ofoafg  42090  ofoaf  42091  ofoaass  42096  naddcnfass  42105  naddwordnexlem4  42138  omssrncard  42277  brtrclfv2  42464  rfovcnvf1od  42741  ntrk0kbimka  42776  isotone1  42785  isotone2  42786  4an4132  43246  mulltgt0  43692  fnchoice  43699  3adantlr3  43710  3adantll2  43711  3adantll3  43712  uzwo4  43726  disjf1o  43875  supxrgelem  44034  infleinflem2  44068  xrralrecnnle  44080  supxrunb3  44096  unb2ltle  44112  infrpgernmpt  44162  iooiinicc  44242  iooiinioc  44256  fmuldfeq  44286  mccl  44301  limccog  44323  limcrecl  44332  lptioo1  44335  islpcn  44342  limsupre  44344  neglimc  44350  0ellimcdiv  44352  limclner  44354  climleltrp  44379  climinf3  44419  liminflimsupclim  44510  xlimpnfxnegmnf  44517  icccncfext  44590  fprodcncf  44603  dvnmptdivc  44641  dvnmul  44646  dvmptfprod  44648  dvnprodlem3  44651  stoweidlem25  44728  stoweidlem34  44737  stoweidlem38  44741  stoweidlem44  44747  stoweidlem48  44751  stoweidlem49  44752  stoweidlem59  44762  stoweidlem60  44763  wallispilem4  44771  stirlinglem5  44781  dirkercncflem2  44807  fourierdlem39  44849  fourierdlem42  44852  fourierdlem46  44855  fourierdlem47  44856  fourierdlem48  44857  fourierdlem50  44859  fourierdlem51  44860  fourierdlem64  44873  fourierdlem73  44882  fourierdlem74  44883  fourierdlem77  44886  fourierdlem80  44889  fourierdlem87  44896  fourierdlem94  44903  fourierdlem103  44912  fourierdlem104  44913  etransclem32  44969  rrxsnicc  45003  sge0cl  45084  sge0f1o  45085  nnfoctbdjlem  45158  ismeannd  45170  omeiunltfirp  45222  hoicvr  45251  ovncvrrp  45267  hoidmvlelem2  45299  hoidmvlelem5  45302  hspdifhsp  45319  hoiqssbllem2  45326  hspmbllem2  45330  vonicclem2  45387  smflimsuplem7  45529  fundcmpsurbijinj  46065  sqrtpwpw2p  46193  isomgrref  46490  lincresunit2  47113  nnpw2pmod  47223  dignn0flhalflem1  47255  dignn0flhalf  47258  rrx2linest  47382  itsclc0yqsol  47404  itsclc0b  47412  functhinclem1  47615  functhinclem2  47616  fullthinc2  47621