Theorem syl21anc 1325

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

Hypotheses

Ref	Expression
syl12anc.1	|- ( ph -> ps )
syl12anc.2	|- ( ph -> ch )
syl12anc.3	|- ( ph -> th )
syl21anc.4	|- ( ( ( ps /\ ch ) /\ th ) -> ta )

Assertion

Ref	Expression
syl21anc	|- ( ph -> ta )

Proof of Theorem syl21anc

Step	Hyp	Ref	Expression
1		syl12anc.1	. . 3 |- ( ph -> ps )
2		syl12anc.2	. . 3 |- ( ph -> ch )
3		syl12anc.3	. . 3 |- ( ph -> th )
4	1, 2, 3	jca31 557	. 2 |- ( ph -> ( ( ps /\ ch ) /\ th ) )
5		syl21anc.4	. 2 |- ( ( ( ps /\ ch ) /\ th ) -> ta )
6	4, 5	syl 17	1 |- ( ph -> ta )

Syntax hints:   -> wi 4   /\ wa 384

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 197  df-an 386

This theorem is referenced by:  wereu2  5111  funprgOLD  5941  funtpg  5942  funtpgOLD  5943  funcnvtp  5951  funcnvqp  5952  funcnvqpOLD  5953  fnunsn  5998  fun2d  6068  fresaun  6075  fvun1  6269  iinpreima  6345  ftpg  6423  fsnunf  6451  f1prex  6539  soisores  6577  isotr  6586  off  6912  caofrss  6930  caonncan  6935  fvmpt2curryd  7397  oaf1o  7643  omeulem1  7662  oeordi  7667  oelimcl  7680  oeeulem  7681  oeeui  7682  oaabs2  7725  omabs  7727  pmresg  7885  ralxpmap  7907  domunsncan  8060  mapunen  8129  sucdom2  8156  unxpdom2  8168  sucxpdom  8169  ac6sfi  8204  unblem4  8215  fodomfi  8239  hartogslem1  8447  brwdom2  8478  cantnflt  8569  cantnflem3  8588  cantnflem4  8589  cnfcomlem  8596  cnfcom  8597  infxpenlem  8836  infxpenc  8841  fseqenlem1  8847  pwsdompw  9026  cfeq0  9078  cofsmo  9091  cfsmolem  9092  ssfin4  9132  hsmexlem4  9251  hsmexlem5  9252  axdc3lem2  9273  axdc3lem4  9275  fpwwe2  9465  wunpr  9531  mulclpi  9715  mulcanenq  9782  distrlem4pr  9848  prlem934  9855  prlem936  9869  divge0d  11912  fseq1p1m1  12414  elfznelfzob  12574  seqcaopr2  12837  facavg  13088  cats1un  13475  f1oun2prg  13662  sqrtdiv  14006  sqrtdivd  14162  mulcn2  14326  o1of2  14343  fsumsplit  14471  sumsplit  14499  isumless  14577  demoivreALT  14931  rpnnen2lem11  14953  gcdnncl  15229  qredeu  15372  rpdvds  15374  isprm5  15419  rpexp  15432  divnumden  15456  divdenle  15457  phimullem  15484  phisum  15495  pythagtriplem4  15524  pythagtriplem8  15528  pythagtriplem9  15529  pcgcd1  15581  sumhash  15600  fldivp1  15601  pockthlem  15609  setsfun  15893  setsfun0  15894  ssc2  16482  estrreslem1  16777  mndpropd  17316  grpidssd  17491  grpinvssd  17492  issubg2  17609  isnsg3  17628  eqgid  17646  gass  17734  symgextres  17845  gsmsymgreqlem2  17851  sylow1lem5  18017  sylow2alem2  18033  sylow3lem3  18044  efgredlemd  18157  efgredlem  18160  frgpnabllem1  18276  frgpnabllem2  18277  subgdmdprd  18433  ablfacrplem  18464  kerf1hrm  18743  issrngd  18861  lmodprop2d  18925  lsspropd  19017  pwssplit1  19059  lspvadd  19096  mplsubglem  19434  mplind  19502  znidomb  19910  znrrg  19914  lindfind  20155  lindsind  20156  mat1ghm  20289  mdetunilem1  20418  mdetunilem3  20420  mdetunilem4  20421  mdetunilem9  20426  cramerimplem2  20490  mat2pmatlin  20540  monmatcollpw  20584  cpmadugsumlemF  20681  mretopd  20896  neiptopnei  20936  neitr  20984  ufilen  21734  flimrest  21787  flimclslem  21788  fclsrest  21828  cnextcn  21871  haustsms2  21940  tsmsxplem2  21957  trust  22033  utoptop  22038  restutop  22041  ustuqtop4  22048  utopsnneiplem  22051  utop2nei  22054  utop3cls  22055  isucn2  22083  ucnima  22085  ucncn  22089  fmucnd  22096  trcfilu  22098  comet  22318  metustexhalf  22361  metustbl  22371  psmetutop  22372  nrmmetd  22379  reconnlem1  22629  reconnlem2  22630  fsumcn  22673  cmetcaulem  23086  iscmet3lem1  23089  iscmet3lem2  23090  bcthlem5  23125  rrxdstprj1  23192  minveclem4  23203  ovolfiniun  23269  itg1addlem4  23466  itg1addlem5  23467  itgsplitioo  23604  c1liplem1  23759  dvfsumlem1  23789  plyeq0lem  23966  quotcan  24064  psercnlem1  24179  cxplea  24442  birthdaylem3  24680  musumsum  24918  dvdsmulf1o  24920  dchrelbas4  24968  dchrhash  24996  gausslemma2dlem0d  25084  gausslemma2dlem1a  25090  2lgslem1a1  25114  2sqlem8a  25150  2sqlem8  25151  chto1ub  25165  vmadivsum  25171  dchrisumlem1  25178  dchrvmasumlem2  25187  dchrvmasumiflem1  25190  rpvmasum2  25201  mulog2sumlem2  25224  selberg2lem  25239  pntrmax  25253  pntpbnd1  25275  pntlemb  25286  pntlemj  25292  ercgrg  25412  tgcgr4  25426  motcgr  25431  tglineeltr  25526  colline  25544  miriso  25565  midexlem  25587  perpneq  25609  foot  25614  f1otrg  25751  f1otrge  25752  axcontlem9  25852  uspgr1ewop  26140  nbupgrres  26266  structtocusgr  26342  wlkp1  26578  clwlkl1loop  26678  uspgrn2crct  26700  crctcshwlkn0lem5  26706  3trlond  27033  3pthond  27035  3spthond  27037  frgr3v  27139  vdgn1frgrv2  27160  numclwwlk3OLD  27242  numclwwlk3  27243  nmblolbii  27654  minvecolem3  27732  minvecolem4  27736  htthlem  27774  bcs2  28039  nmopub2tALT  28768  nmfnleub2  28785  eighmorth  28823  nmophmi  28890  nmopcoadji  28960  hstle  29089  atcvat3i  29255  disjxpin  29401  fmptco1f1o  29434  off2  29443  xppreima2  29450  fgreu  29471  1stpreimas  29483  padct  29497  resf1o  29505  fpwrelmap  29508  xrofsup  29533  eliccelico  29539  elicoelioo  29540  iocinif  29543  difioo  29544  2sqcoprm  29647  2sqmod  29648  ressprs  29655  tleile  29661  xrge0addgt0  29691  xrge0adddir  29692  omndmul3  29713  archirng  29742  archirngz  29743  gsumle  29779  orngmul  29803  1smat1  29870  madjusmdetlem2  29894  qtophaus  29903  locfinref  29908  metideq  29936  sqsscirc2  29955  tpr2rico  29958  fmcncfil  29977  lmxrge0  29998  lmdvg  29999  qqhval2lem  30025  qqhf  30030  qqhnm  30034  esumle  30120  gsumesum  30121  esumlef  30124  esumrnmpt2  30130  esumpcvgval  30140  esum2d  30155  ofcf  30165  ldsysgenld  30223  ldgenpisyslem1  30226  unelros  30234  difelros  30235  inelsros  30241  diffiunisros  30242  imambfm  30324  omssubadd  30362  inelcarsg  30373  carsgsigalem  30377  carsggect  30380  carsgclctunlem2  30381  oddpwdc  30416  eulerpartlems  30422  eulerpartlemb  30430  eulerpartlemt  30433  iwrdsplit  30449  sseqfn  30452  sseqf  30454  sseqfres  30455  ballotlemfc0  30554  ballotlemfcc  30555  ballotlemfrcn0  30591  sgnsub  30606  plymulx0  30624  signsplypnf  30627  signsvtn0  30647  signstfvneq0  30649  signsvtp  30660  signsvtn  30661  fsum2dsub  30685  reprlt  30697  hashreprin  30698  reprgt  30699  reprpmtf1o  30704  chtvalz  30707  breprexplema  30708  breprexplemc  30710  breprexp  30711  circlemeth  30718  logdivsqrle  30728  hgt750lemb  30734  bnj927  30839  bnj1536  30924  bnj1001  31028  bnj1280  31088  cvxsconn  31225  elmrsubrn  31417  noextend  31819  neibastop3  32357  finxpsuclem  33234  poimirlem16  33425  poimirlem19  33428  poimirlem20  33429  poimirlem29  33438  mblfinlem3  33448  itg2addnclem3  33463  ftc1cnnclem  33483  lautlt  35377  lautcvr  35378  lauteq  35381  lautco  35383  ltrncl  35411  ltrncnvleN  35416  trljat2  35454  cdlemc6  35483  cdleme20c  35599  cdleme20j  35606  cdleme22e  35632  cdleme22eALTN  35633  cdlemg7aN  35913  cdlemg12e  35935  cdlemg17dALTN  35952  cdlemh  36105  cdlemkfid1N  36209  dibglbN  36455  diblss  36459  diclspsn  36483  dih1  36575  dihglbcpreN  36589  dihmeetlem4preN  36595  lcfrlem19  36850  mapfzcons  37279  mzpcl34  37294  mzpindd  37309  mzpsubst  37311  diophrw  37322  diophren  37377  irrapxlem1  37386  pellexlem5  37397  acongrep  37547  pwssplit4  37659  brtrclfv2  38019  rfovcnvf1od  38298  ntrk0kbimka  38337  isotone1  38346  isotone2  38347  4an4132  38705  mulltgt0  39181  fnchoice  39188  3adantlr3  39200  3adantll2  39202  3adantll3  39203  uzwo4  39221  disjf1o  39378  supxrgelem  39553  infleinflem2  39587  xrralrecnnle  39602  supxrunb3  39623  unb2ltle  39642  infrpgernmpt  39695  iooiinicc  39769  iooiinioc  39783  fmuldfeq  39815  mccl  39830  limccog  39852  limcrecl  39861  lptioo1  39864  islpcn  39871  limsupre  39873  neglimc  39879  0ellimcdiv  39881  limclner  39883  climleltrp  39908  climinf3  39948  liminflimsupclim  40039  icccncfext  40100  fprodcncf  40114  dvnmptdivc  40153  dvnmul  40158  dvmptfprod  40160  dvnprodlem3  40163  stoweidlem25  40242  stoweidlem34  40251  stoweidlem38  40255  stoweidlem44  40261  stoweidlem48  40265  stoweidlem49  40266  stoweidlem59  40276  stoweidlem60  40277  wallispilem4  40285  stirlinglem5  40295  dirkercncflem2  40321  fourierdlem39  40363  fourierdlem42  40366  fourierdlem46  40369  fourierdlem47  40370  fourierdlem48  40371  fourierdlem50  40373  fourierdlem51  40374  fourierdlem64  40387  fourierdlem73  40396  fourierdlem74  40397  fourierdlem77  40400  fourierdlem80  40403  fourierdlem87  40410  fourierdlem94  40417  fourierdlem103  40426  fourierdlem104  40427  etransclem32  40483  rrxsnicc  40520  sge0cl  40598  sge0f1o  40599  nnfoctbdjlem  40672  ismeannd  40684  omeiunltfirp  40733  hoicvr  40762  ovncvrrp  40778  hoidmvlelem2  40810  hoidmvlelem5  40813  hspdifhsp  40830  hoiqssbllem2  40837  hspmbllem2  40841  vonicclem2  40898  smflimsuplem7  41032  sqrtpwpw2p  41450  lincresunit2  42267  nnpw2pmod  42377  dignn0flhalflem1  42409  dignn0flhalf  42412