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  4237  ordelord  4364  wetriext  4559  releldm  4844  relelrn  4845  f1imass  5751  ovmpodxf  5976  ovmpodf  5982  fovrnd  5995  offval  6066  caoftrn  6084  offval3  6111  fnmpoovd  6192  tfrlemisucaccv  6302  tfrlemiubacc  6307  tfr1onlemsucaccv  6318  tfr1onlembfn  6321  tfrcllemsucaccv  6331  tfrcllembfn  6334  rdgss  6360  rdgisuc1  6361  rdgisucinc  6362  frecrdg  6385  mapsspm  6658  en2d  6744  en3d  6745  dom3d  6750  ssdomg  6754  f1imaen2g  6769  2dom  6781  cnven  6784  mapen  6822  mapxpen  6824  phpelm  6842  fidifsnen  6846  dif1en  6855  dif1enen  6856  diffisn  6869  isinfinf  6873  unfidisj  6897  unfiin  6901  tpfidisj  6903  xpfi  6905  fisseneq  6907  phpeqd  6908  ssfirab  6909  fnfi  6912  f1dmvrnfibi  6919  iunfidisj  6921  f1finf1o  6922  en1eqsn  6923  fidcenumlemr  6930  updjudhcoinlf  7055  updjudhcoinrg  7056  difinfinf  7076  en2eleq  7165  en2other2  7166  dju1en  7183  djuassen  7187  xpdjuen  7188  addcmpblnq  7322  addassnqg  7337  distrnqg  7342  ltsonq  7353  ltanqg  7355  ltmnqg  7356  ltaddnq  7362  ltexnqq  7363  prarloclemarch  7373  ltrnqg  7375  addcmpblnq0  7398  nnanq0  7413  distrnq0  7414  addassnq0  7417  prarloclemlt  7448  prarloclemcalc  7457  addnqprllem  7482  addnqprulem  7483  addnqprl  7484  addnqpru  7485  addlocprlemgt  7489  appdivnq  7518  prmuloclemcalc  7520  mulnqprl  7523  mulnqpru  7524  mullocprlem  7525  distrlem4prl  7539  distrlem4pru  7540  ltprordil  7544  ltexprlemopl  7556  ltexprlemopu  7558  ltexprlemloc  7562  ltexprlemru  7567  addcanprleml  7569  addcanprlemu  7570  ltaprlem  7573  ltaprg  7574  addextpr  7576  recexprlem1ssu  7589  aptipr  7596  ltmprr  7597  caucvgprlemcanl  7599  cauappcvgprlemopl  7601  cauappcvgprlemdisj  7606  cauappcvgprlemloc  7607  cauappcvgprlemladdfu  7609  cauappcvgprlemladdru  7611  cauappcvgprlemladdrl  7612  cauappcvgprlem1  7614  caucvgprlemm  7623  caucvgprlemopl  7624  caucvgprlemloc  7630  caucvgprlemladdfu  7632  caucvgprlemladdrl  7633  caucvgprprlemloccalc  7639  caucvgprprlemml  7649  caucvgprprlemopl  7652  caucvgprprlemloc  7658  caucvgprprlemexb  7662  caucvgprprlemaddq  7663  caucvgprprlem1  7664  caucvgprprlem2  7665  suplocexprlemmu  7673  suplocexprlemru  7674  addcmpblnr  7694  mulcmpblnrlemg  7695  mulcmpblnr  7696  ltsrprg  7702  distrsrg  7714  lttrsr  7717  ltsosr  7719  1idsr  7723  ltasrg  7725  recexgt0sr  7728  mulgt0sr  7733  mulextsr1lem  7735  srpospr  7738  prsradd  7741  prsrlt  7742  caucvgsrlemoffval  7751  caucvgsrlemoffgt1  7754  caucvgsrlemoffres  7755  caucvgsr  7757  ltpsrprg  7758  map2psrprg  7760  suplocsrlemb  7761  suplocsrlempr  7762  suplocsrlem  7763  pitoregt0  7804  recidpirqlemcalc  7812  axmulass  7828  axdistr  7829  rereceu  7844  recriota  7845  addassd  7935  mulassd  7936  adddid  7937  adddird  7938  lelttr  8001  letrd  8036  lelttrd  8037  lttrd  8038  mul12d  8064  mul32d  8065  mul31d  8066  add12d  8079  add32d  8080  cnegexlem3  8089  addcand  8096  addcan2d  8097  pncan  8118  pncan3  8120  subcan2  8137  subsub2  8140  subsub4  8145  npncan3  8150  pnpcan  8151  pnncan  8153  addsub4  8155  subaddd  8241  subadd2d  8242  addsubassd  8243  addsubd  8244  subadd23d  8245  addsub12d  8246  npncand  8247  nppcand  8248  nppcan2d  8249  nppcan3d  8250  subsubd  8251  subsub2d  8252  subsub3d  8253  subsub4d  8254  sub32d  8255  nnncand  8256  nnncan1d  8257  nnncan2d  8258  npncan3d  8259  pnpcand  8260  pnpcan2d  8261  pnncand  8262  ppncand  8263  subcand  8264  subcan2d  8265  subcanad  8266  subcan2ad  8268  subdid  8326  subdird  8327  ltadd2  8331  ltadd2d  8333  ltletrd  8335  ltsubadd  8344  lesubadd  8346  ltaddsub  8348  leaddsub  8350  le2add  8356  lt2add  8357  ltleadd  8358  lesub1  8368  lesub2  8369  ltsub1  8370  ltsub2  8371  lt2sub  8372  le2sub  8373  subge0  8387  lesub0  8391  ltadd1d  8450  leadd1d  8451  leadd2d  8452  ltsubaddd  8453  lesubaddd  8454  ltsubadd2d  8455  lesubadd2d  8456  ltaddsubd  8457  ltaddsub2d  8458  leaddsub2d  8459  subled  8460  lesubd  8461  ltsub23d  8462  ltsub13d  8463  lesub1d  8464  lesub2d  8465  ltsub1d  8466  ltsub2d  8467  gt0add  8485  apcotr  8519  apadd1  8520  addext  8522  mulext1  8524  mulext  8526  gtapd  8549  leltapd  8551  mulap0  8565  mul0eqap  8581  divvalap  8584  divcanap2  8590  diveqap0  8592  divrecap  8598  divassap  8600  divmulassap  8605  divmulasscomap  8606  divdirap  8607  divcanap3  8608  div11ap  8610  rec11ap  8620  divmuldivap  8622  divdivdivap  8623  divmuleqap  8627  dmdcanap  8632  ddcanap  8636  divadddivap  8637  divsubdivap  8638  redivclap  8641  apmul1  8698  divclapd  8700  divcanap1d  8701  divcanap2d  8702  divrecapd  8703  divrecap2d  8704  divcanap3d  8705  divcanap4d  8706  diveqap0d  8707  diveqap1d  8708  diveqap1ad  8709  diveqap0ad  8710  divap0bd  8712  divnegapd  8713  divneg2apd  8714  div2negapd  8715  redivclapd  8745  div2subap  8747  ltmul12a  8769  lemul12b  8770  lt2mul2div  8788  ltdiv2  8796  ltdiv23  8801  avglt1  9109  avglt2  9110  lt2halvesd  9118  div4p1lem1div2  9124  zltp1le  9259  elz2  9276  zdivmul  9295  uztrn  9496  eluzsub  9509  uz3m2nn  9525  qaddcl  9587  elpq  9600  cnref1o  9602  ltdiv2d  9670  lediv2d  9671  divlt1lt  9674  divle1le  9675  ledivge1le  9676  ltmulgt11d  9682  ltmulgt12d  9683  gt0divd  9684  ge0divd  9685  rpgecld  9686  ltmul1d  9688  ltmul2d  9689  lemul1d  9690  lemul2d  9691  ltdiv1d  9692  lediv1d  9693  ltmuldivd  9694  ltmuldiv2d  9695  lemuldivd  9696  lemuldiv2d  9697  ltdivmuld  9698  ltdivmul2d  9699  ledivmuld  9700  ledivmul2d  9701  ltdiv23d  9707  lediv23d  9708  addlelt  9718  xrltso  9746  xrlelttr  9756  xrlttrd  9759  xrlelttrd  9760  xrltletrd  9761  xrletrd  9762  xrre3  9772  xleadd1  9825  xltadd1  9826  xle2add  9829  xlt2add  9830  xlesubadd  9833  xadd4d  9835  ixxss1  9854  ixxss2  9855  ixxss12  9856  iooshf  9902  icoshftf1o  9941  ioodisj  9943  zltaddlt1le  9957  fznlem  9990  fzdifsuc  10030  fzrev  10033  fzrevral2  10055  elfz0fzfz0  10075  elfzmlbp  10081  fzctr  10082  elfzole1  10104  elfzolt2  10105  fzoss2  10121  fzospliti  10125  fzo1fzo0n0  10132  elfzo0z  10133  fzofzim  10137  fzoaddel  10141  eluzgtdifelfzo  10146  elfzodifsumelfzo  10150  ssfzo12bi  10174  elfzonelfzo  10179  fvinim0ffz  10190  rebtwn2zlemstep  10202  rebtwn2z  10204  qbtwnxr  10207  flqge  10231  2tnp1ge0ge0  10250  intfracq  10269  flqdiv  10270  modqval  10273  modqcld  10277  modqmulnn  10291  zmodcl  10293  zmodfz  10295  modqid  10298  zmodid2  10301  modqabs  10306  modqcyc  10308  modqadd1  10310  modqaddabs  10311  modqaddmod  10312  mulp1mod1  10314  modqmuladd  10315  modqmuladdim  10316  modqmuladdnn0  10317  m1modnnsub1  10319  modqltm1p1mod  10325  modqmul1  10326  modqsubmod  10331  modqsubmodmod  10332  q2txmodxeq0  10333  modaddmodup  10336  modqmulmod  10338  modqaddmulmod  10340  modqdi  10341  modqsubdir  10342  addmodlteq  10347  frecuzrdgrrn  10357  frec2uzrdg  10358  frecuzrdgrcl  10359  frecuzrdgsuc  10363  frecuzrdgrclt  10364  frecuzrdgg  10365  frecuzrdgsuctlem  10372  frecfzen2  10376  seq3val  10407  seqvalcd  10408  seqf  10410  seq3p1  10411  seqovcd  10412  seqp1cd  10415  monoord  10425  iseqf1olemqcl  10435  iseqf1olemnab  10437  iseqf1olemmo  10441  iseqf1olemqk  10443  seq3f1olemqsumkj  10447  seq3f1olemstep  10450  expnnval  10472  expnegap0  10477  rpexpcl  10488  expnegzap  10503  expgt1  10507  mulexpzap  10509  exprecap  10510  expaddzaplem  10512  expaddzap  10513  expmul  10514  expmulzap  10515  expdivap  10520  ltexp2a  10521  leexp2a  10522  leexp2r  10523  leexp1a  10524  bernneq2  10590  bernneq3  10591  expnbnd  10592  expnlbnd  10593  expnlbnd2  10594  expaddd  10604  expmuld  10605  expclzapd  10607  expap0d  10608  expnegapd  10609  exprecapd  10610  expp1zapd  10611  expm1apd  10612  sqdivapd  10615  mulexpd  10617  expge0d  10620  expge1d  10621  sqoddm1div8  10622  reexpclzapd  10627  leexp2ad  10631  facwordi  10667  faclbnd3  10670  facavg  10673  bcval  10676  bccmpl  10681  bc0k  10683  bcval5  10690  bcpasc  10693  hashfiv01gt1  10709  hashunlem  10732  hashunsng  10735  fiprsshashgt1  10745  hashdifsn  10747  hashdifpr  10748  hashfz  10749  hashxp  10754  fiubm  10756  hashfacen  10764  zfz1isolemiso  10767  zfz1isolem1  10768  zfz1iso  10769  shftfvalg  10775  seq3shft  10795  mulreap  10821  cjreb  10823  cjap  10863  cnrecnv  10867  cjdivapd  10925  redivapd  10931  imdivapd  10932  resqrexlemdecn  10969  absexpzap  11037  abslt  11045  absle  11046  elicc4abs  11051  abs3lem  11068  fzomaxdiflem  11069  cau3lem  11071  amgm2  11075  abssubge0d  11133  abssuble0d  11134  absdifltd  11135  absdifled  11136  absdivapd  11152  abs3difd  11157  qdenre  11159  maxabslemlub  11164  rexanre  11177  rexico  11178  fimaxre2  11183  lemininf  11190  ltmininf  11191  rpmincl  11194  mul0inf  11197  xrmaxiflemlub  11204  xrmaxltsup  11214  xrmaxaddlem  11216  xrmaxadd  11217  xrltmininf  11226  xrlemininf  11227  xrminltinf  11228  xrminadd  11231  xrbdtri  11232  climshftlemg  11258  climshft2  11262  addcn2  11266  mulcn2  11268  reccn2ap  11269  cn1lem  11270  climadd  11282  climmul  11283  climsub  11284  climsqz  11291  climsqz2  11292  climrecvg1n  11304  climcvg1nlem  11305  fisumss  11348  fsumsplitsn  11366  sumpr  11369  fsumsplitsnun  11375  fsum2dlemstep  11390  fisumcom2  11394  fisum0diag2  11403  fsumconst  11410  modfsummodlemstep  11413  fsumlessfi  11416  fsumabs  11421  fsumiun  11433  hashiun  11434  hash2iun  11435  hash2iun1dif1  11436  binomlem  11439  bcxmas  11445  isumshft  11446  isumlessdc  11452  expcnvap0  11458  expcnvre  11459  geosergap  11462  cvgratnnlembern  11479  cvgratnnlemnexp  11480  cvgratnnlemmn  11481  mertenslemi1  11491  fprodssdc  11546  fprodm1  11554  fprodunsn  11560  fprodeq0  11573  fprod2dlemstep  11578  fprodcom2fi  11582  fprodsplitsn  11589  fprodsplit1f  11590  efaddlem  11630  eftlub  11646  efltim  11654  eirraplem  11732  dvdsval3  11746  nndivdvds  11751  modm1div  11755  summodnegmod  11777  modmulconst  11778  dvds2subd  11782  dvds2addd  11784  dvdstrd  11785  dvdsmultr1d  11787  dvdsmultr2  11788  dvdsabseq  11800  dvdsfac  11813  dvdsmod  11815  oddge22np1  11833  ltoddhalfle  11845  halfleoddlt  11846  nn0ehalf  11855  nno  11858  nn0oddm1d2  11861  divalglemnn  11870  divalg  11876  divalgmod  11879  fldivndvdslt  11887  flodddiv4lt  11888  flodddiv4t2lthalf  11889  infssuzex  11897  dvdsbnd  11904  gcdneg  11930  gcdaddm  11932  modgcd  11939  gcdmultipled  11941  dvdsgcdidd  11942  bezoutlemnewy  11944  bezoutlemstep  11945  bezoutlembi  11953  dvdsgcdb  11961  gcdass  11963  mulgcd  11964  dvdsmulgcd  11973  rpmulgcd  11974  sqgcd  11977  nnwodc  11984  uzwodc  11985  nn0seqcvgd  11988  eucalglt  12004  gcddvdslcm  12020  lcmgcdlem  12024  lcmdvdsb  12031  lcmass  12032  ncoprmgcdne1b  12036  coprmdvds2  12040  mulgcddvds  12041  rpmulgcd2  12042  qredeu  12044  rpdvds  12046  divgcdcoprm0  12048  cncongr1  12050  cncongr2  12051  isprm2lem  12063  prmind2  12067  nprm  12070  dvdsnprmd  12072  exprmfct  12085  prmdvdsfz  12086  isprm5lem  12088  divgcdodd  12090  isprm6  12094  prmdvdsexp  12095  prmexpb  12098  prmfac1  12099  rpexp  12100  rpexp12i  12102  pw2dvdseulemle  12114  sqpweven  12122  2sqpwodd  12123  divnumden  12143  numdensq  12149  nonsq  12154  hashdvds  12168  phiprmpw  12169  crth  12171  phimullem  12172  eulerthlem1  12174  eulerthlemfi  12175  eulerthlemrprm  12176  eulerthlema  12177  eulerthlemh  12178  eulerthlemth  12179  prmdiv  12182  prmdiveq  12183  prmdivdiv  12184  hashgcdlem  12185  phisum  12187  odzdvds  12192  odzphi  12193  vfermltl  12198  powm2modprm  12199  reumodprminv  12200  modprm0  12201  nnnn0modprm0  12202  modprmn0modprm0  12203  coprimeprodsq  12204  pythagtriplem4  12215  pythagtriplem19  12229  pclemub  12234  pcprendvds2  12238  pcpremul  12240  pcval  12243  pcdiv  12249  pcqdiv  12254  pcexp  12256  pcdvdsb  12266  pcidlem  12269  pcdvdstr  12273  pcgcd1  12274  pc2dvds  12276  pcprmpw2  12279  dvdsprmpweqle  12283  pcaddlem  12285  pcadd  12286  pcmpt  12288  pcmptdvds  12290  fldivp1  12293  pcfaclem  12294  pcfac  12295  pcbc  12296  oddprmdvds  12299  prmpwdvds  12300  pockthlem  12301  pockthg  12302  1arith  12312  4sqlem5  12327  4sqlem6  12328  4sqlem7  12329  4sqlem8  12330  4sqlem9  12331  4sqlem4  12337  ennnfonelemp1  12354  ennnfonelemex  12362  ennnfonelemrn  12367  ctinfom  12376  ctiunct  12388  nninfdclemcl  12396  nninfdclemp1  12398  strsetsid  12442  fvsetsid  12443  setsabsd  12448  setscom  12449  ressid2  12470  ressval2  12471  srngstrd  12533  lmodstrd  12544  ipsstrd  12552  topgrpstrd  12562  plusfvalg  12610  opifismgmdc  12618  mnd4g  12658  mndpfo  12667  mndpropd  12669  mhmf1o  12686  issubmd  12689  mndissubm  12690  mhmco  12698  mhmima  12699  mhmeql  12700  grpcld  12714  difopn  12867  uncld  12872  ntrin  12883  clsss2  12888  ntrcls0  12890  topssnei  12921  neissex  12924  restbasg  12927  tgrest  12928  resttopon  12930  restabs  12934  restopnb  12940  cnpfval  12954  cnprcl2k  12965  tgcnp  12968  iscnp4  12977  cnpnei  12978  cnptopco  12981  cncnpi  12987  cncnp  12989  cnconst2  12992  cnrest  12994  cnrest2  12995  cnrest2r  12996  cnptopresti  12997  cnptoprest  12998  cnptoprest2  12999  lmss  13005  lmtopcnp  13009  txvalex  13013  txval  13014  txbasval  13026  txcnp  13030  txcnmpt  13032  txcn  13034  txdis1cn  13037  lmcn2  13039  cnmptc  13041  cnmpt11  13042  cnmpt1t  13044  cnmpt12  13046  cnmpt21  13050  cnmpt2t  13052  cnmpt22  13053  cnmpt22f  13054  cnmptcom  13057  hmeores  13074  txhmeo  13078  psmettri  13089  xmettri  13131  metrtri  13136  xmetres2  13138  blfvalps  13144  bldisj  13160  blgt0  13161  xblss2ps  13163  xblss2  13164  blhalf  13167  blininf  13183  blssps  13186  blss  13187  blssexps  13188  blssex  13189  blin2  13191  xmeter  13195  blnei  13251  blsscls2  13252  metss2lem  13256  bdmetval  13259  bdxmet  13260  bdbl  13262  xmetxp  13266  xmetxpbl  13267  xmettxlem  13268  xmettx  13269  metcnp3  13270  metcnp  13271  metcnp2  13272  metcnpi  13274  metcnpi2  13275  metcnpi3  13276  txmetcnp  13277  metcnpd  13279  tgqioo  13306  addcncntoplem  13310  fsumcncntop  13315  mulc1cncf  13335  cncfco  13337  mulcncflem  13349  mulcncf  13350  suplociccreex  13361  suplociccex  13362  dedekindicc  13370  ivthinclemlm  13371  ivthinclemum  13372  ivthinclemlopn  13373  ivthinclemuopn  13375  ivthinclemloc  13378  ivthdec  13381  limccl  13387  ellimc3apf  13388  limcimolemlt  13392  cnplimclemle  13396  cnplimclemr  13397  limccnpcntop  13403  limccnp2lem  13404  limccnp2cntop  13405  reldvg  13407  eldvap  13410  dvbssntrcntop  13412  dvcnp2cntop  13422  dvmulxxbr  13425  dvrecap  13436  dveflem  13446  reeff1o  13453  efltlemlt  13454  sin0pilem2  13462  ptolemy  13504  sinq12gt0  13510  cxprec  13590  rpcxproot  13593  cxpmuld  13615  rpabscxpbnd  13618  rplogbval  13622  rplogbchbase  13627  relogbval  13628  relogbzcl  13629  rplogbreexp  13630  rprelogbmul  13632  rprelogbdiv  13634  nnlogbexp  13636  relogbcxpbap  13642  logbgt0b  13643  logbgcd1irr  13644  logbgcd1irraplemexp  13645  logbgcd1irraplemap  13646  logbprmirr  13649  lgslem1  13660  lgslem4  13663  lgsval2lem  13670  lgsvalmod  13679  lgsval4a  13682  lgsneg  13684  lgsmod  13686  lgsdirprm  13694  lgsdir  13695  lgsdilem2  13696  lgsdi  13697  lgsne0  13698  2sqlem2  13710  2sqlem3  13712  2sqlem4  13713  2sqlem6  13715  2sqlem8  13718  apdifflemr  14044  apdiff  14045  iswomni0  14048