Theorem syl3anc 1228

Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Hypotheses

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

Assertion

Ref	Expression
syl3anc	|- ( ph -> ta )

Proof of Theorem syl3anc

Step	Hyp	Ref	Expression
1		sylXanc.1	. . 3 |- ( ph -> ps )
2		sylXanc.2	. . 3 |- ( ph -> ch )
3		sylXanc.3	. . 3 |- ( ph -> th )
4	1, 2, 3	3jca 1167	. 2 |- ( ph -> ( ps /\ ch /\ th ) )
5		syl111anc.4	. 2 |- ( ( ps /\ ch /\ th ) -> ta )
6	4, 5	syl 14	1 |- ( ph -> ta )

Syntax hints:   -> wi 4   /\ w3a 968

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 970

This theorem is referenced by:  syl112anc  1232  syl121anc  1233  syl211anc  1234  syl113anc  1240  syl131anc  1241  syl311anc  1242  syld3an3  1273  3jaod  1294  mpd3an23  1329  stoic4a  1420  rspc3ev  2847  sbciedf  2986  euotd  4232  ordelord  4359  wetriext  4554  releldm  4839  relelrn  4840  f1imass  5742  ovmpodxf  5967  ovmpodf  5973  fovrnd  5986  offval  6057  caoftrn  6075  offval3  6102  fnmpoovd  6183  tfrlemisucaccv  6293  tfrlemiubacc  6298  tfr1onlemsucaccv  6309  tfr1onlembfn  6312  tfrcllemsucaccv  6322  tfrcllembfn  6325  rdgss  6351  rdgisuc1  6352  rdgisucinc  6353  frecrdg  6376  mapsspm  6648  en2d  6734  en3d  6735  dom3d  6740  ssdomg  6744  f1imaen2g  6759  2dom  6771  cnven  6774  mapen  6812  mapxpen  6814  phpelm  6832  fidifsnen  6836  dif1en  6845  dif1enen  6846  diffisn  6859  isinfinf  6863  unfidisj  6887  unfiin  6891  tpfidisj  6893  xpfi  6895  fisseneq  6897  phpeqd  6898  ssfirab  6899  fnfi  6902  f1dmvrnfibi  6909  iunfidisj  6911  f1finf1o  6912  en1eqsn  6913  fidcenumlemr  6920  updjudhcoinlf  7045  updjudhcoinrg  7046  difinfinf  7066  en2eleq  7151  en2other2  7152  dju1en  7169  djuassen  7173  xpdjuen  7174  addcmpblnq  7308  addassnqg  7323  distrnqg  7328  ltsonq  7339  ltanqg  7341  ltmnqg  7342  ltaddnq  7348  ltexnqq  7349  prarloclemarch  7359  ltrnqg  7361  addcmpblnq0  7384  nnanq0  7399  distrnq0  7400  addassnq0  7403  prarloclemlt  7434  prarloclemcalc  7443  addnqprllem  7468  addnqprulem  7469  addnqprl  7470  addnqpru  7471  addlocprlemgt  7475  appdivnq  7504  prmuloclemcalc  7506  mulnqprl  7509  mulnqpru  7510  mullocprlem  7511  distrlem4prl  7525  distrlem4pru  7526  ltprordil  7530  ltexprlemopl  7542  ltexprlemopu  7544  ltexprlemloc  7548  ltexprlemru  7553  addcanprleml  7555  addcanprlemu  7556  ltaprlem  7559  ltaprg  7560  addextpr  7562  recexprlem1ssu  7575  aptipr  7582  ltmprr  7583  caucvgprlemcanl  7585  cauappcvgprlemopl  7587  cauappcvgprlemdisj  7592  cauappcvgprlemloc  7593  cauappcvgprlemladdfu  7595  cauappcvgprlemladdru  7597  cauappcvgprlemladdrl  7598  cauappcvgprlem1  7600  caucvgprlemm  7609  caucvgprlemopl  7610  caucvgprlemloc  7616  caucvgprlemladdfu  7618  caucvgprlemladdrl  7619  caucvgprprlemloccalc  7625  caucvgprprlemml  7635  caucvgprprlemopl  7638  caucvgprprlemloc  7644  caucvgprprlemexb  7648  caucvgprprlemaddq  7649  caucvgprprlem1  7650  caucvgprprlem2  7651  suplocexprlemmu  7659  suplocexprlemru  7660  addcmpblnr  7680  mulcmpblnrlemg  7681  mulcmpblnr  7682  ltsrprg  7688  distrsrg  7700  lttrsr  7703  ltsosr  7705  1idsr  7709  ltasrg  7711  recexgt0sr  7714  mulgt0sr  7719  mulextsr1lem  7721  srpospr  7724  prsradd  7727  prsrlt  7728  caucvgsrlemoffval  7737  caucvgsrlemoffgt1  7740  caucvgsrlemoffres  7741  caucvgsr  7743  ltpsrprg  7744  map2psrprg  7746  suplocsrlemb  7747  suplocsrlempr  7748  suplocsrlem  7749  pitoregt0  7790  recidpirqlemcalc  7798  axmulass  7814  axdistr  7815  rereceu  7830  recriota  7831  addassd  7921  mulassd  7922  adddid  7923  adddird  7924  lelttr  7987  letrd  8022  lelttrd  8023  lttrd  8024  mul12d  8050  mul32d  8051  mul31d  8052  add12d  8065  add32d  8066  cnegexlem3  8075  addcand  8082  addcan2d  8083  pncan  8104  pncan3  8106  subcan2  8123  subsub2  8126  subsub4  8131  npncan3  8136  pnpcan  8137  pnncan  8139  addsub4  8141  subaddd  8227  subadd2d  8228  addsubassd  8229  addsubd  8230  subadd23d  8231  addsub12d  8232  npncand  8233  nppcand  8234  nppcan2d  8235  nppcan3d  8236  subsubd  8237  subsub2d  8238  subsub3d  8239  subsub4d  8240  sub32d  8241  nnncand  8242  nnncan1d  8243  nnncan2d  8244  npncan3d  8245  pnpcand  8246  pnpcan2d  8247  pnncand  8248  ppncand  8249  subcand  8250  subcan2d  8251  subcanad  8252  subcan2ad  8254  subdid  8312  subdird  8313  ltadd2  8317  ltadd2d  8319  ltletrd  8321  ltsubadd  8330  lesubadd  8332  ltaddsub  8334  leaddsub  8336  le2add  8342  lt2add  8343  ltleadd  8344  lesub1  8354  lesub2  8355  ltsub1  8356  ltsub2  8357  lt2sub  8358  le2sub  8359  subge0  8373  lesub0  8377  ltadd1d  8436  leadd1d  8437  leadd2d  8438  ltsubaddd  8439  lesubaddd  8440  ltsubadd2d  8441  lesubadd2d  8442  ltaddsubd  8443  ltaddsub2d  8444  leaddsub2d  8445  subled  8446  lesubd  8447  ltsub23d  8448  ltsub13d  8449  lesub1d  8450  lesub2d  8451  ltsub1d  8452  ltsub2d  8453  gt0add  8471  apcotr  8505  apadd1  8506  addext  8508  mulext1  8510  mulext  8512  gtapd  8535  leltapd  8537  mulap0  8551  mul0eqap  8567  divvalap  8570  divcanap2  8576  diveqap0  8578  divrecap  8584  divassap  8586  divmulassap  8591  divmulasscomap  8592  divdirap  8593  divcanap3  8594  div11ap  8596  rec11ap  8606  divmuldivap  8608  divdivdivap  8609  divmuleqap  8613  dmdcanap  8618  ddcanap  8622  divadddivap  8623  divsubdivap  8624  redivclap  8627  apmul1  8684  divclapd  8686  divcanap1d  8687  divcanap2d  8688  divrecapd  8689  divrecap2d  8690  divcanap3d  8691  divcanap4d  8692  diveqap0d  8693  diveqap1d  8694  diveqap1ad  8695  diveqap0ad  8696  divap0bd  8698  divnegapd  8699  divneg2apd  8700  div2negapd  8701  redivclapd  8731  div2subap  8733  ltmul12a  8755  lemul12b  8756  lt2mul2div  8774  ltdiv2  8782  ltdiv23  8787  avglt1  9095  avglt2  9096  lt2halvesd  9104  div4p1lem1div2  9110  zltp1le  9245  elz2  9262  zdivmul  9281  uztrn  9482  eluzsub  9495  uz3m2nn  9511  qaddcl  9573  elpq  9586  cnref1o  9588  ltdiv2d  9656  lediv2d  9657  divlt1lt  9660  divle1le  9661  ledivge1le  9662  ltmulgt11d  9668  ltmulgt12d  9669  gt0divd  9670  ge0divd  9671  rpgecld  9672  ltmul1d  9674  ltmul2d  9675  lemul1d  9676  lemul2d  9677  ltdiv1d  9678  lediv1d  9679  ltmuldivd  9680  ltmuldiv2d  9681  lemuldivd  9682  lemuldiv2d  9683  ltdivmuld  9684  ltdivmul2d  9685  ledivmuld  9686  ledivmul2d  9687  ltdiv23d  9693  lediv23d  9694  addlelt  9704  xrltso  9732  xrlelttr  9742  xrlttrd  9745  xrlelttrd  9746  xrltletrd  9747  xrletrd  9748  xrre3  9758  xleadd1  9811  xltadd1  9812  xle2add  9815  xlt2add  9816  xlesubadd  9819  xadd4d  9821  ixxss1  9840  ixxss2  9841  ixxss12  9842  iooshf  9888  icoshftf1o  9927  ioodisj  9929  zltaddlt1le  9943  fznlem  9976  fzdifsuc  10016  fzrev  10019  fzrevral2  10041  elfz0fzfz0  10061  elfzmlbp  10067  fzctr  10068  elfzole1  10090  elfzolt2  10091  fzoss2  10107  fzospliti  10111  fzo1fzo0n0  10118  elfzo0z  10119  fzofzim  10123  fzoaddel  10127  eluzgtdifelfzo  10132  elfzodifsumelfzo  10136  ssfzo12bi  10160  elfzonelfzo  10165  fvinim0ffz  10176  rebtwn2zlemstep  10188  rebtwn2z  10190  qbtwnxr  10193  flqge  10217  2tnp1ge0ge0  10236  intfracq  10255  flqdiv  10256  modqval  10259  modqcld  10263  modqmulnn  10277  zmodcl  10279  zmodfz  10281  modqid  10284  zmodid2  10287  modqabs  10292  modqcyc  10294  modqadd1  10296  modqaddabs  10297  modqaddmod  10298  mulp1mod1  10300  modqmuladd  10301  modqmuladdim  10302  modqmuladdnn0  10303  m1modnnsub1  10305  modqltm1p1mod  10311  modqmul1  10312  modqsubmod  10317  modqsubmodmod  10318  q2txmodxeq0  10319  modaddmodup  10322  modqmulmod  10324  modqaddmulmod  10326  modqdi  10327  modqsubdir  10328  addmodlteq  10333  frecuzrdgrrn  10343  frec2uzrdg  10344  frecuzrdgrcl  10345  frecuzrdgsuc  10349  frecuzrdgrclt  10350  frecuzrdgg  10351  frecuzrdgsuctlem  10358  frecfzen2  10362  seq3val  10393  seqvalcd  10394  seqf  10396  seq3p1  10397  seqovcd  10398  seqp1cd  10401  monoord  10411  iseqf1olemqcl  10421  iseqf1olemnab  10423  iseqf1olemmo  10427  iseqf1olemqk  10429  seq3f1olemqsumkj  10433  seq3f1olemstep  10436  expnnval  10458  expnegap0  10463  rpexpcl  10474  expnegzap  10489  expgt1  10493  mulexpzap  10495  exprecap  10496  expaddzaplem  10498  expaddzap  10499  expmul  10500  expmulzap  10501  expdivap  10506  ltexp2a  10507  leexp2a  10508  leexp2r  10509  leexp1a  10510  bernneq2  10576  bernneq3  10577  expnbnd  10578  expnlbnd  10579  expnlbnd2  10580  expaddd  10590  expmuld  10591  expclzapd  10593  expap0d  10594  expnegapd  10595  exprecapd  10596  expp1zapd  10597  expm1apd  10598  sqdivapd  10601  mulexpd  10603  expge0d  10606  expge1d  10607  sqoddm1div8  10608  reexpclzapd  10613  leexp2ad  10617  facwordi  10653  faclbnd3  10656  facavg  10659  bcval  10662  bccmpl  10667  bc0k  10669  bcval5  10676  bcpasc  10679  hashfiv01gt1  10695  hashunlem  10717  hashunsng  10720  fiprsshashgt1  10730  hashdifsn  10732  hashdifpr  10733  hashfz  10734  hashxp  10739  fiubm  10741  hashfacen  10749  zfz1isolemiso  10752  zfz1isolem1  10753  zfz1iso  10754  shftfvalg  10760  seq3shft  10780  mulreap  10806  cjreb  10808  cjap  10848  cnrecnv  10852  cjdivapd  10910  redivapd  10916  imdivapd  10917  resqrexlemdecn  10954  absexpzap  11022  abslt  11030  absle  11031  elicc4abs  11036  abs3lem  11053  fzomaxdiflem  11054  cau3lem  11056  amgm2  11060  abssubge0d  11118  abssuble0d  11119  absdifltd  11120  absdifled  11121  absdivapd  11137  abs3difd  11142  qdenre  11144  maxabslemlub  11149  rexanre  11162  rexico  11163  fimaxre2  11168  lemininf  11175  ltmininf  11176  rpmincl  11179  mul0inf  11182  xrmaxiflemlub  11189  xrmaxltsup  11199  xrmaxaddlem  11201  xrmaxadd  11202  xrltmininf  11211  xrlemininf  11212  xrminltinf  11213  xrminadd  11216  xrbdtri  11217  climshftlemg  11243  climshft2  11247  addcn2  11251  mulcn2  11253  reccn2ap  11254  cn1lem  11255  climadd  11267  climmul  11268  climsub  11269  climsqz  11276  climsqz2  11277  climrecvg1n  11289  climcvg1nlem  11290  fisumss  11333  fsumsplitsn  11351  sumpr  11354  fsumsplitsnun  11360  fsum2dlemstep  11375  fisumcom2  11379  fisum0diag2  11388  fsumconst  11395  modfsummodlemstep  11398  fsumlessfi  11401  fsumabs  11406  fsumiun  11418  hashiun  11419  hash2iun  11420  hash2iun1dif1  11421  binomlem  11424  bcxmas  11430  isumshft  11431  isumlessdc  11437  expcnvap0  11443  expcnvre  11444  geosergap  11447  cvgratnnlembern  11464  cvgratnnlemnexp  11465  cvgratnnlemmn  11466  mertenslemi1  11476  fprodssdc  11531  fprodm1  11539  fprodunsn  11545  fprodeq0  11558  fprod2dlemstep  11563  fprodcom2fi  11567  fprodsplitsn  11574  fprodsplit1f  11575  efaddlem  11615  eftlub  11631  efltim  11639  eirraplem  11717  dvdsval3  11731  nndivdvds  11736  modm1div  11740  summodnegmod  11762  modmulconst  11763  dvds2subd  11767  dvds2addd  11769  dvdstrd  11770  dvdsmultr1d  11772  dvdsmultr2  11773  dvdsabseq  11785  dvdsfac  11798  dvdsmod  11800  oddge22np1  11818  ltoddhalfle  11830  halfleoddlt  11831  nn0ehalf  11840  nno  11843  nn0oddm1d2  11846  divalglemnn  11855  divalg  11861  divalgmod  11864  fldivndvdslt  11872  flodddiv4lt  11873  flodddiv4t2lthalf  11874  infssuzex  11882  dvdsbnd  11889  gcdneg  11915  gcdaddm  11917  modgcd  11924  gcdmultipled  11926  dvdsgcdidd  11927  bezoutlemnewy  11929  bezoutlemstep  11930  bezoutlembi  11938  dvdsgcdb  11946  gcdass  11948  mulgcd  11949  dvdsmulgcd  11958  rpmulgcd  11959  sqgcd  11962  nnwodc  11969  uzwodc  11970  nn0seqcvgd  11973  eucalglt  11989  gcddvdslcm  12005  lcmgcdlem  12009  lcmdvdsb  12016  lcmass  12017  ncoprmgcdne1b  12021  coprmdvds2  12025  mulgcddvds  12026  rpmulgcd2  12027  qredeu  12029  rpdvds  12031  divgcdcoprm0  12033  cncongr1  12035  cncongr2  12036  isprm2lem  12048  prmind2  12052  nprm  12055  dvdsnprmd  12057  exprmfct  12070  prmdvdsfz  12071  isprm5lem  12073  divgcdodd  12075  isprm6  12079  prmdvdsexp  12080  prmexpb  12083  prmfac1  12084  rpexp  12085  rpexp12i  12087  pw2dvdseulemle  12099  sqpweven  12107  2sqpwodd  12108  divnumden  12128  numdensq  12134  nonsq  12139  hashdvds  12153  phiprmpw  12154  crth  12156  phimullem  12157  eulerthlem1  12159  eulerthlemfi  12160  eulerthlemrprm  12161  eulerthlema  12162  eulerthlemh  12163  eulerthlemth  12164  prmdiv  12167  prmdiveq  12168  prmdivdiv  12169  hashgcdlem  12170  phisum  12172  odzdvds  12177  odzphi  12178  vfermltl  12183  powm2modprm  12184  reumodprminv  12185  modprm0  12186  nnnn0modprm0  12187  modprmn0modprm0  12188  coprimeprodsq  12189  pythagtriplem4  12200  pythagtriplem19  12214  pclemub  12219  pcprendvds2  12223  pcpremul  12225  pcval  12228  pcdiv  12234  pcqdiv  12239  pcexp  12241  pcdvdsb  12251  pcidlem  12254  pcdvdstr  12258  pcgcd1  12259  pc2dvds  12261  pcprmpw2  12264  dvdsprmpweqle  12268  pcaddlem  12270  pcadd  12271  pcmpt  12273  pcmptdvds  12275  fldivp1  12278  pcfaclem  12279  pcfac  12280  pcbc  12281  oddprmdvds  12284  prmpwdvds  12285  pockthlem  12286  pockthg  12287  1arith  12297  4sqlem5  12312  4sqlem6  12313  4sqlem7  12314  4sqlem8  12315  4sqlem9  12316  4sqlem4  12322  ennnfonelemp1  12339  ennnfonelemex  12347  ennnfonelemrn  12352  ctinfom  12361  ctiunct  12373  nninfdclemcl  12381  nninfdclemp1  12383  strsetsid  12427  fvsetsid  12428  setsabsd  12433  setscom  12434  ressid2  12454  ressval2  12455  srngstrd  12517  lmodstrd  12528  ipsstrd  12536  topgrpstrd  12546  plusfvalg  12594  opifismgmdc  12602  difopn  12758  uncld  12763  ntrin  12774  clsss2  12779  ntrcls0  12781  topssnei  12812  neissex  12815  restbasg  12818  tgrest  12819  resttopon  12821  restabs  12825  restopnb  12831  cnpfval  12845  cnprcl2k  12856  tgcnp  12859  iscnp4  12868  cnpnei  12869  cnptopco  12872  cncnpi  12878  cncnp  12880  cnconst2  12883  cnrest  12885  cnrest2  12886  cnrest2r  12887  cnptopresti  12888  cnptoprest  12889  cnptoprest2  12890  lmss  12896  lmtopcnp  12900  txvalex  12904  txval  12905  txbasval  12917  txcnp  12921  txcnmpt  12923  txcn  12925  txdis1cn  12928  lmcn2  12930  cnmptc  12932  cnmpt11  12933  cnmpt1t  12935  cnmpt12  12937  cnmpt21  12941  cnmpt2t  12943  cnmpt22  12944  cnmpt22f  12945  cnmptcom  12948  hmeores  12965  txhmeo  12969  psmettri  12980  xmettri  13022  metrtri  13027  xmetres2  13029  blfvalps  13035  bldisj  13051  blgt0  13052  xblss2ps  13054  xblss2  13055  blhalf  13058  blininf  13074  blssps  13077  blss  13078  blssexps  13079  blssex  13080  blin2  13082  xmeter  13086  blnei  13142  blsscls2  13143  metss2lem  13147  bdmetval  13150  bdxmet  13151  bdbl  13153  xmetxp  13157  xmetxpbl  13158  xmettxlem  13159  xmettx  13160  metcnp3  13161  metcnp  13162  metcnp2  13163  metcnpi  13165  metcnpi2  13166  metcnpi3  13167  txmetcnp  13168  metcnpd  13170  tgqioo  13197  addcncntoplem  13201  fsumcncntop  13206  mulc1cncf  13226  cncfco  13228  mulcncflem  13240  mulcncf  13241  suplociccreex  13252  suplociccex  13253  dedekindicc  13261  ivthinclemlm  13262  ivthinclemum  13263  ivthinclemlopn  13264  ivthinclemuopn  13266  ivthinclemloc  13269  ivthdec  13272  limccl  13278  ellimc3apf  13279  limcimolemlt  13283  cnplimclemle  13287  cnplimclemr  13288  limccnpcntop  13294  limccnp2lem  13295  limccnp2cntop  13296  reldvg  13298  eldvap  13301  dvbssntrcntop  13303  dvcnp2cntop  13313  dvmulxxbr  13316  dvrecap  13327  dveflem  13337  reeff1o  13344  efltlemlt  13345  sin0pilem2  13353  ptolemy  13395  sinq12gt0  13401  cxprec  13481  rpcxproot  13484  cxpmuld  13506  rpabscxpbnd  13509  rplogbval  13513  rplogbchbase  13518  relogbval  13519  relogbzcl  13520  rplogbreexp  13521  rprelogbmul  13523  rprelogbdiv  13525  nnlogbexp  13527  relogbcxpbap  13533  logbgt0b  13534  logbgcd1irr  13535  logbgcd1irraplemexp  13536  logbgcd1irraplemap  13537  logbprmirr  13540  lgslem1  13551  lgslem4  13554  lgsval2lem  13561  lgsvalmod  13570  lgsval4a  13573  lgsneg  13575  lgsmod  13577  lgsdirprm  13585  lgsdir  13586  lgsdilem2  13587  lgsdi  13588  lgsne0  13589  2sqlem2  13601  2sqlem3  13603  2sqlem4  13604  2sqlem6  13606  2sqlem8  13609  apdifflemr  13936  apdiff  13937  iswomni0  13940