Theorem syl3anc 1233

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 1172	. 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 973

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 975

This theorem is referenced by:  syl112anc  1237  syl121anc  1238  syl211anc  1239  syl113anc  1245  syl131anc  1246  syl311anc  1247  syld3an3  1278  3jaod  1299  mpd3an23  1334  stoic4a  1425  rspc3ev  2851  sbciedf  2990  euotd  4239  ordelord  4366  wetriext  4561  releldm  4846  relelrn  4847  f1imass  5753  ovmpodxf  5978  ovmpodf  5984  fovrnd  5997  offval  6068  caoftrn  6086  offval3  6113  fnmpoovd  6194  tfrlemisucaccv  6304  tfrlemiubacc  6309  tfr1onlemsucaccv  6320  tfr1onlembfn  6323  tfrcllemsucaccv  6333  tfrcllembfn  6336  rdgss  6362  rdgisuc1  6363  rdgisucinc  6364  frecrdg  6387  mapsspm  6660  en2d  6746  en3d  6747  dom3d  6752  ssdomg  6756  f1imaen2g  6771  2dom  6783  cnven  6786  mapen  6824  mapxpen  6826  phpelm  6844  fidifsnen  6848  dif1en  6857  dif1enen  6858  diffisn  6871  isinfinf  6875  unfidisj  6899  unfiin  6903  tpfidisj  6905  xpfi  6907  fisseneq  6909  phpeqd  6910  ssfirab  6911  fnfi  6914  f1dmvrnfibi  6921  iunfidisj  6923  f1finf1o  6924  en1eqsn  6925  fidcenumlemr  6932  updjudhcoinlf  7057  updjudhcoinrg  7058  difinfinf  7078  en2eleq  7172  en2other2  7173  dju1en  7190  djuassen  7194  xpdjuen  7195  addcmpblnq  7329  addassnqg  7344  distrnqg  7349  ltsonq  7360  ltanqg  7362  ltmnqg  7363  ltaddnq  7369  ltexnqq  7370  prarloclemarch  7380  ltrnqg  7382  addcmpblnq0  7405  nnanq0  7420  distrnq0  7421  addassnq0  7424  prarloclemlt  7455  prarloclemcalc  7464  addnqprllem  7489  addnqprulem  7490  addnqprl  7491  addnqpru  7492  addlocprlemgt  7496  appdivnq  7525  prmuloclemcalc  7527  mulnqprl  7530  mulnqpru  7531  mullocprlem  7532  distrlem4prl  7546  distrlem4pru  7547  ltprordil  7551  ltexprlemopl  7563  ltexprlemopu  7565  ltexprlemloc  7569  ltexprlemru  7574  addcanprleml  7576  addcanprlemu  7577  ltaprlem  7580  ltaprg  7581  addextpr  7583  recexprlem1ssu  7596  aptipr  7603  ltmprr  7604  caucvgprlemcanl  7606  cauappcvgprlemopl  7608  cauappcvgprlemdisj  7613  cauappcvgprlemloc  7614  cauappcvgprlemladdfu  7616  cauappcvgprlemladdru  7618  cauappcvgprlemladdrl  7619  cauappcvgprlem1  7621  caucvgprlemm  7630  caucvgprlemopl  7631  caucvgprlemloc  7637  caucvgprlemladdfu  7639  caucvgprlemladdrl  7640  caucvgprprlemloccalc  7646  caucvgprprlemml  7656  caucvgprprlemopl  7659  caucvgprprlemloc  7665  caucvgprprlemexb  7669  caucvgprprlemaddq  7670  caucvgprprlem1  7671  caucvgprprlem2  7672  suplocexprlemmu  7680  suplocexprlemru  7681  addcmpblnr  7701  mulcmpblnrlemg  7702  mulcmpblnr  7703  ltsrprg  7709  distrsrg  7721  lttrsr  7724  ltsosr  7726  1idsr  7730  ltasrg  7732  recexgt0sr  7735  mulgt0sr  7740  mulextsr1lem  7742  srpospr  7745  prsradd  7748  prsrlt  7749  caucvgsrlemoffval  7758  caucvgsrlemoffgt1  7761  caucvgsrlemoffres  7762  caucvgsr  7764  ltpsrprg  7765  map2psrprg  7767  suplocsrlemb  7768  suplocsrlempr  7769  suplocsrlem  7770  pitoregt0  7811  recidpirqlemcalc  7819  axmulass  7835  axdistr  7836  rereceu  7851  recriota  7852  addassd  7942  mulassd  7943  adddid  7944  adddird  7945  lelttr  8008  letrd  8043  lelttrd  8044  lttrd  8045  mul12d  8071  mul32d  8072  mul31d  8073  add12d  8086  add32d  8087  cnegexlem3  8096  addcand  8103  addcan2d  8104  pncan  8125  pncan3  8127  subcan2  8144  subsub2  8147  subsub4  8152  npncan3  8157  pnpcan  8158  pnncan  8160  addsub4  8162  subaddd  8248  subadd2d  8249  addsubassd  8250  addsubd  8251  subadd23d  8252  addsub12d  8253  npncand  8254  nppcand  8255  nppcan2d  8256  nppcan3d  8257  subsubd  8258  subsub2d  8259  subsub3d  8260  subsub4d  8261  sub32d  8262  nnncand  8263  nnncan1d  8264  nnncan2d  8265  npncan3d  8266  pnpcand  8267  pnpcan2d  8268  pnncand  8269  ppncand  8270  subcand  8271  subcan2d  8272  subcanad  8273  subcan2ad  8275  subdid  8333  subdird  8334  ltadd2  8338  ltadd2d  8340  ltletrd  8342  ltsubadd  8351  lesubadd  8353  ltaddsub  8355  leaddsub  8357  le2add  8363  lt2add  8364  ltleadd  8365  lesub1  8375  lesub2  8376  ltsub1  8377  ltsub2  8378  lt2sub  8379  le2sub  8380  subge0  8394  lesub0  8398  ltadd1d  8457  leadd1d  8458  leadd2d  8459  ltsubaddd  8460  lesubaddd  8461  ltsubadd2d  8462  lesubadd2d  8463  ltaddsubd  8464  ltaddsub2d  8465  leaddsub2d  8466  subled  8467  lesubd  8468  ltsub23d  8469  ltsub13d  8470  lesub1d  8471  lesub2d  8472  ltsub1d  8473  ltsub2d  8474  gt0add  8492  apcotr  8526  apadd1  8527  addext  8529  mulext1  8531  mulext  8533  gtapd  8556  leltapd  8558  mulap0  8572  mul0eqap  8588  divvalap  8591  divcanap2  8597  diveqap0  8599  divrecap  8605  divassap  8607  divmulassap  8612  divmulasscomap  8613  divdirap  8614  divcanap3  8615  div11ap  8617  rec11ap  8627  divmuldivap  8629  divdivdivap  8630  divmuleqap  8634  dmdcanap  8639  ddcanap  8643  divadddivap  8644  divsubdivap  8645  redivclap  8648  apmul1  8705  divclapd  8707  divcanap1d  8708  divcanap2d  8709  divrecapd  8710  divrecap2d  8711  divcanap3d  8712  divcanap4d  8713  diveqap0d  8714  diveqap1d  8715  diveqap1ad  8716  diveqap0ad  8717  divap0bd  8719  divnegapd  8720  divneg2apd  8721  div2negapd  8722  redivclapd  8752  div2subap  8754  ltmul12a  8776  lemul12b  8777  lt2mul2div  8795  ltdiv2  8803  ltdiv23  8808  avglt1  9116  avglt2  9117  lt2halvesd  9125  div4p1lem1div2  9131  zltp1le  9266  elz2  9283  zdivmul  9302  uztrn  9503  eluzsub  9516  uz3m2nn  9532  qaddcl  9594  elpq  9607  cnref1o  9609  ltdiv2d  9677  lediv2d  9678  divlt1lt  9681  divle1le  9682  ledivge1le  9683  ltmulgt11d  9689  ltmulgt12d  9690  gt0divd  9691  ge0divd  9692  rpgecld  9693  ltmul1d  9695  ltmul2d  9696  lemul1d  9697  lemul2d  9698  ltdiv1d  9699  lediv1d  9700  ltmuldivd  9701  ltmuldiv2d  9702  lemuldivd  9703  lemuldiv2d  9704  ltdivmuld  9705  ltdivmul2d  9706  ledivmuld  9707  ledivmul2d  9708  ltdiv23d  9714  lediv23d  9715  addlelt  9725  xrltso  9753  xrlelttr  9763  xrlttrd  9766  xrlelttrd  9767  xrltletrd  9768  xrletrd  9769  xrre3  9779  xleadd1  9832  xltadd1  9833  xle2add  9836  xlt2add  9837  xlesubadd  9840  xadd4d  9842  ixxss1  9861  ixxss2  9862  ixxss12  9863  iooshf  9909  icoshftf1o  9948  ioodisj  9950  zltaddlt1le  9964  fznlem  9997  fzdifsuc  10037  fzrev  10040  fzrevral2  10062  elfz0fzfz0  10082  elfzmlbp  10088  fzctr  10089  elfzole1  10111  elfzolt2  10112  fzoss2  10128  fzospliti  10132  fzo1fzo0n0  10139  elfzo0z  10140  fzofzim  10144  fzoaddel  10148  eluzgtdifelfzo  10153  elfzodifsumelfzo  10157  ssfzo12bi  10181  elfzonelfzo  10186  fvinim0ffz  10197  rebtwn2zlemstep  10209  rebtwn2z  10211  qbtwnxr  10214  flqge  10238  2tnp1ge0ge0  10257  intfracq  10276  flqdiv  10277  modqval  10280  modqcld  10284  modqmulnn  10298  zmodcl  10300  zmodfz  10302  modqid  10305  zmodid2  10308  modqabs  10313  modqcyc  10315  modqadd1  10317  modqaddabs  10318  modqaddmod  10319  mulp1mod1  10321  modqmuladd  10322  modqmuladdim  10323  modqmuladdnn0  10324  m1modnnsub1  10326  modqltm1p1mod  10332  modqmul1  10333  modqsubmod  10338  modqsubmodmod  10339  q2txmodxeq0  10340  modaddmodup  10343  modqmulmod  10345  modqaddmulmod  10347  modqdi  10348  modqsubdir  10349  addmodlteq  10354  frecuzrdgrrn  10364  frec2uzrdg  10365  frecuzrdgrcl  10366  frecuzrdgsuc  10370  frecuzrdgrclt  10371  frecuzrdgg  10372  frecuzrdgsuctlem  10379  frecfzen2  10383  seq3val  10414  seqvalcd  10415  seqf  10417  seq3p1  10418  seqovcd  10419  seqp1cd  10422  monoord  10432  iseqf1olemqcl  10442  iseqf1olemnab  10444  iseqf1olemmo  10448  iseqf1olemqk  10450  seq3f1olemqsumkj  10454  seq3f1olemstep  10457  expnnval  10479  expnegap0  10484  rpexpcl  10495  expnegzap  10510  expgt1  10514  mulexpzap  10516  exprecap  10517  expaddzaplem  10519  expaddzap  10520  expmul  10521  expmulzap  10522  expdivap  10527  ltexp2a  10528  leexp2a  10529  leexp2r  10530  leexp1a  10531  bernneq2  10597  bernneq3  10598  expnbnd  10599  expnlbnd  10600  expnlbnd2  10601  expaddd  10611  expmuld  10612  expclzapd  10614  expap0d  10615  expnegapd  10616  exprecapd  10617  expp1zapd  10618  expm1apd  10619  sqdivapd  10622  mulexpd  10624  expge0d  10627  expge1d  10628  sqoddm1div8  10629  reexpclzapd  10634  leexp2ad  10638  facwordi  10674  faclbnd3  10677  facavg  10680  bcval  10683  bccmpl  10688  bc0k  10690  bcval5  10697  bcpasc  10700  hashfiv01gt1  10716  hashunlem  10739  hashunsng  10742  fiprsshashgt1  10752  hashdifsn  10754  hashdifpr  10755  hashfz  10756  hashxp  10761  fiubm  10763  hashfacen  10771  zfz1isolemiso  10774  zfz1isolem1  10775  zfz1iso  10776  shftfvalg  10782  seq3shft  10802  mulreap  10828  cjreb  10830  cjap  10870  cnrecnv  10874  cjdivapd  10932  redivapd  10938  imdivapd  10939  resqrexlemdecn  10976  absexpzap  11044  abslt  11052  absle  11053  elicc4abs  11058  abs3lem  11075  fzomaxdiflem  11076  cau3lem  11078  amgm2  11082  abssubge0d  11140  abssuble0d  11141  absdifltd  11142  absdifled  11143  absdivapd  11159  abs3difd  11164  qdenre  11166  maxabslemlub  11171  rexanre  11184  rexico  11185  fimaxre2  11190  lemininf  11197  ltmininf  11198  rpmincl  11201  mul0inf  11204  xrmaxiflemlub  11211  xrmaxltsup  11221  xrmaxaddlem  11223  xrmaxadd  11224  xrltmininf  11233  xrlemininf  11234  xrminltinf  11235  xrminadd  11238  xrbdtri  11239  climshftlemg  11265  climshft2  11269  addcn2  11273  mulcn2  11275  reccn2ap  11276  cn1lem  11277  climadd  11289  climmul  11290  climsub  11291  climsqz  11298  climsqz2  11299  climrecvg1n  11311  climcvg1nlem  11312  fisumss  11355  fsumsplitsn  11373  sumpr  11376  fsumsplitsnun  11382  fsum2dlemstep  11397  fisumcom2  11401  fisum0diag2  11410  fsumconst  11417  modfsummodlemstep  11420  fsumlessfi  11423  fsumabs  11428  fsumiun  11440  hashiun  11441  hash2iun  11442  hash2iun1dif1  11443  binomlem  11446  bcxmas  11452  isumshft  11453  isumlessdc  11459  expcnvap0  11465  expcnvre  11466  geosergap  11469  cvgratnnlembern  11486  cvgratnnlemnexp  11487  cvgratnnlemmn  11488  mertenslemi1  11498  fprodssdc  11553  fprodm1  11561  fprodunsn  11567  fprodeq0  11580  fprod2dlemstep  11585  fprodcom2fi  11589  fprodsplitsn  11596  fprodsplit1f  11597  efaddlem  11637  eftlub  11653  efltim  11661  eirraplem  11739  dvdsval3  11753  nndivdvds  11758  modm1div  11762  summodnegmod  11784  modmulconst  11785  dvds2subd  11789  dvds2addd  11791  dvdstrd  11792  dvdsmultr1d  11794  dvdsmultr2  11795  dvdsabseq  11807  dvdsfac  11820  dvdsmod  11822  oddge22np1  11840  ltoddhalfle  11852  halfleoddlt  11853  nn0ehalf  11862  nno  11865  nn0oddm1d2  11868  divalglemnn  11877  divalg  11883  divalgmod  11886  fldivndvdslt  11894  flodddiv4lt  11895  flodddiv4t2lthalf  11896  infssuzex  11904  dvdsbnd  11911  gcdneg  11937  gcdaddm  11939  modgcd  11946  gcdmultipled  11948  dvdsgcdidd  11949  bezoutlemnewy  11951  bezoutlemstep  11952  bezoutlembi  11960  dvdsgcdb  11968  gcdass  11970  mulgcd  11971  dvdsmulgcd  11980  rpmulgcd  11981  sqgcd  11984  nnwodc  11991  uzwodc  11992  nn0seqcvgd  11995  eucalglt  12011  gcddvdslcm  12027  lcmgcdlem  12031  lcmdvdsb  12038  lcmass  12039  ncoprmgcdne1b  12043  coprmdvds2  12047  mulgcddvds  12048  rpmulgcd2  12049  qredeu  12051  rpdvds  12053  divgcdcoprm0  12055  cncongr1  12057  cncongr2  12058  isprm2lem  12070  prmind2  12074  nprm  12077  dvdsnprmd  12079  exprmfct  12092  prmdvdsfz  12093  isprm5lem  12095  divgcdodd  12097  isprm6  12101  prmdvdsexp  12102  prmexpb  12105  prmfac1  12106  rpexp  12107  rpexp12i  12109  pw2dvdseulemle  12121  sqpweven  12129  2sqpwodd  12130  divnumden  12150  numdensq  12156  nonsq  12161  hashdvds  12175  phiprmpw  12176  crth  12178  phimullem  12179  eulerthlem1  12181  eulerthlemfi  12182  eulerthlemrprm  12183  eulerthlema  12184  eulerthlemh  12185  eulerthlemth  12186  prmdiv  12189  prmdiveq  12190  prmdivdiv  12191  hashgcdlem  12192  phisum  12194  odzdvds  12199  odzphi  12200  vfermltl  12205  powm2modprm  12206  reumodprminv  12207  modprm0  12208  nnnn0modprm0  12209  modprmn0modprm0  12210  coprimeprodsq  12211  pythagtriplem4  12222  pythagtriplem19  12236  pclemub  12241  pcprendvds2  12245  pcpremul  12247  pcval  12250  pcdiv  12256  pcqdiv  12261  pcexp  12263  pcdvdsb  12273  pcidlem  12276  pcdvdstr  12280  pcgcd1  12281  pc2dvds  12283  pcprmpw2  12286  dvdsprmpweqle  12290  pcaddlem  12292  pcadd  12293  pcmpt  12295  pcmptdvds  12297  fldivp1  12300  pcfaclem  12301  pcfac  12302  pcbc  12303  oddprmdvds  12306  prmpwdvds  12307  pockthlem  12308  pockthg  12309  1arith  12319  4sqlem5  12334  4sqlem6  12335  4sqlem7  12336  4sqlem8  12337  4sqlem9  12338  4sqlem4  12344  ennnfonelemp1  12361  ennnfonelemex  12369  ennnfonelemrn  12374  ctinfom  12383  ctiunct  12395  nninfdclemcl  12403  nninfdclemp1  12405  strsetsid  12449  fvsetsid  12450  setsabsd  12455  setscom  12456  ressid2  12477  ressval2  12478  srngstrd  12540  lmodstrd  12551  ipsstrd  12559  topgrpstrd  12569  plusfvalg  12617  opifismgmdc  12625  mnd4g  12665  mndpfo  12674  mndpropd  12676  mhmf1o  12693  issubmd  12696  mndissubm  12697  mhmco  12705  mhmima  12706  mhmeql  12707  grpcld  12721  grpsubval  12749  difopn  12902  uncld  12907  ntrin  12918  clsss2  12923  ntrcls0  12925  topssnei  12956  neissex  12959  restbasg  12962  tgrest  12963  resttopon  12965  restabs  12969  restopnb  12975  cnpfval  12989  cnprcl2k  13000  tgcnp  13003  iscnp4  13012  cnpnei  13013  cnptopco  13016  cncnpi  13022  cncnp  13024  cnconst2  13027  cnrest  13029  cnrest2  13030  cnrest2r  13031  cnptopresti  13032  cnptoprest  13033  cnptoprest2  13034  lmss  13040  lmtopcnp  13044  txvalex  13048  txval  13049  txbasval  13061  txcnp  13065  txcnmpt  13067  txcn  13069  txdis1cn  13072  lmcn2  13074  cnmptc  13076  cnmpt11  13077  cnmpt1t  13079  cnmpt12  13081  cnmpt21  13085  cnmpt2t  13087  cnmpt22  13088  cnmpt22f  13089  cnmptcom  13092  hmeores  13109  txhmeo  13113  psmettri  13124  xmettri  13166  metrtri  13171  xmetres2  13173  blfvalps  13179  bldisj  13195  blgt0  13196  xblss2ps  13198  xblss2  13199  blhalf  13202  blininf  13218  blssps  13221  blss  13222  blssexps  13223  blssex  13224  blin2  13226  xmeter  13230  blnei  13286  blsscls2  13287  metss2lem  13291  bdmetval  13294  bdxmet  13295  bdbl  13297  xmetxp  13301  xmetxpbl  13302  xmettxlem  13303  xmettx  13304  metcnp3  13305  metcnp  13306  metcnp2  13307  metcnpi  13309  metcnpi2  13310  metcnpi3  13311  txmetcnp  13312  metcnpd  13314  tgqioo  13341  addcncntoplem  13345  fsumcncntop  13350  mulc1cncf  13370  cncfco  13372  mulcncflem  13384  mulcncf  13385  suplociccreex  13396  suplociccex  13397  dedekindicc  13405  ivthinclemlm  13406  ivthinclemum  13407  ivthinclemlopn  13408  ivthinclemuopn  13410  ivthinclemloc  13413  ivthdec  13416  limccl  13422  ellimc3apf  13423  limcimolemlt  13427  cnplimclemle  13431  cnplimclemr  13432  limccnpcntop  13438  limccnp2lem  13439  limccnp2cntop  13440  reldvg  13442  eldvap  13445  dvbssntrcntop  13447  dvcnp2cntop  13457  dvmulxxbr  13460  dvrecap  13471  dveflem  13481  reeff1o  13488  efltlemlt  13489  sin0pilem2  13497  ptolemy  13539  sinq12gt0  13545  cxprec  13625  rpcxproot  13628  cxpmuld  13650  rpabscxpbnd  13653  rplogbval  13657  rplogbchbase  13662  relogbval  13663  relogbzcl  13664  rplogbreexp  13665  rprelogbmul  13667  rprelogbdiv  13669  nnlogbexp  13671  relogbcxpbap  13677  logbgt0b  13678  logbgcd1irr  13679  logbgcd1irraplemexp  13680  logbgcd1irraplemap  13681  logbprmirr  13684  lgslem1  13695  lgslem4  13698  lgsval2lem  13705  lgsvalmod  13714  lgsval4a  13717  lgsneg  13719  lgsmod  13721  lgsdirprm  13729  lgsdir  13730  lgsdilem2  13731  lgsdi  13732  lgsne0  13733  2sqlem2  13745  2sqlem3  13747  2sqlem4  13748  2sqlem6  13750  2sqlem8  13753  apdifflemr  14079  apdiff  14080  iswomni0  14083