Theorem syl3anc 1184

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 1129	. 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 930

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

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

This theorem is referenced by:  syl112anc  1188  syl121anc  1189  syl211anc  1190  syl113anc  1196  syl131anc  1197  syl311anc  1198  syld3an3  1229  3jaod  1250  mpd3an23  1285  stoic4a  1376  rspc3ev  2760  sbciedf  2896  euotd  4114  ordelord  4241  wetriext  4429  releldm  4712  relelrn  4713  f1imass  5607  ovmpodxf  5828  ovmpodf  5834  fovrnd  5847  offval  5921  fnofval  5923  caoftrn  5938  offval3  5963  fnmpoovd  6042  tfrlemisucaccv  6152  tfrlemiubacc  6157  tfr1onlemsucaccv  6168  tfr1onlembfn  6171  tfrcllemsucaccv  6181  tfrcllembfn  6184  rdgss  6210  rdgisuc1  6211  rdgisucinc  6212  frecrdg  6235  mapsspm  6506  en2d  6592  en3d  6593  dom3d  6598  ssdomg  6602  f1imaen2g  6617  2dom  6629  cnven  6632  mapen  6669  mapxpen  6671  phpelm  6689  fidifsnen  6693  dif1en  6702  dif1enen  6703  diffisn  6716  isinfinf  6720  unfidisj  6739  unfiin  6743  tpfidisj  6745  xpfi  6747  fisseneq  6749  ssfirab  6750  fnfi  6753  f1dmvrnfibi  6760  iunfidisj  6762  f1finf1o  6763  en1eqsn  6764  fidcenumlemr  6771  updjudhcoinlf  6880  updjudhcoinrg  6881  difinfinf  6901  en2eleq  6960  en2other2  6961  dju1en  6973  djuassen  6977  xpdjuen  6978  addcmpblnq  7076  addassnqg  7091  distrnqg  7096  ltsonq  7107  ltanqg  7109  ltmnqg  7110  ltaddnq  7116  ltexnqq  7117  prarloclemarch  7127  ltrnqg  7129  addcmpblnq0  7152  nnanq0  7167  distrnq0  7168  addassnq0  7171  prarloclemlt  7202  prarloclemcalc  7211  addnqprllem  7236  addnqprulem  7237  addnqprl  7238  addnqpru  7239  addlocprlemgt  7243  appdivnq  7272  prmuloclemcalc  7274  mulnqprl  7277  mulnqpru  7278  mullocprlem  7279  distrlem4prl  7293  distrlem4pru  7294  ltprordil  7298  ltexprlemopl  7310  ltexprlemopu  7312  ltexprlemloc  7316  ltexprlemru  7321  addcanprleml  7323  addcanprlemu  7324  ltaprlem  7327  ltaprg  7328  addextpr  7330  recexprlem1ssu  7343  aptipr  7350  ltmprr  7351  caucvgprlemcanl  7353  cauappcvgprlemopl  7355  cauappcvgprlemdisj  7360  cauappcvgprlemloc  7361  cauappcvgprlemladdfu  7363  cauappcvgprlemladdru  7365  cauappcvgprlemladdrl  7366  cauappcvgprlem1  7368  caucvgprlemm  7377  caucvgprlemopl  7378  caucvgprlemloc  7384  caucvgprlemladdfu  7386  caucvgprlemladdrl  7387  caucvgprprlemloccalc  7393  caucvgprprlemml  7403  caucvgprprlemopl  7406  caucvgprprlemloc  7412  caucvgprprlemexb  7416  caucvgprprlemaddq  7417  caucvgprprlem1  7418  caucvgprprlem2  7419  addcmpblnr  7435  mulcmpblnrlemg  7436  mulcmpblnr  7437  ltsrprg  7443  distrsrg  7455  lttrsr  7458  ltsosr  7460  1idsr  7464  ltasrg  7466  recexgt0sr  7469  mulgt0sr  7473  mulextsr1lem  7475  srpospr  7478  prsradd  7481  prsrlt  7482  caucvgsrlemoffval  7491  caucvgsrlemoffgt1  7494  caucvgsrlemoffres  7495  caucvgsr  7497  pitoregt0  7536  recidpirqlemcalc  7544  axmulass  7558  axdistr  7559  rereceu  7574  recriota  7575  addassd  7660  mulassd  7661  adddid  7662  adddird  7663  lelttr  7723  letrd  7757  lelttrd  7758  lttrd  7759  mul12d  7785  mul32d  7786  mul31d  7787  add12d  7800  add32d  7801  cnegexlem3  7810  addcand  7817  addcan2d  7818  pncan  7839  pncan3  7841  subcan2  7858  subsub2  7861  subsub4  7866  npncan3  7871  pnpcan  7872  pnncan  7874  addsub4  7876  subaddd  7962  subadd2d  7963  addsubassd  7964  addsubd  7965  subadd23d  7966  addsub12d  7967  npncand  7968  nppcand  7969  nppcan2d  7970  nppcan3d  7971  subsubd  7972  subsub2d  7973  subsub3d  7974  subsub4d  7975  sub32d  7976  nnncand  7977  nnncan1d  7978  nnncan2d  7979  npncan3d  7980  pnpcand  7981  pnpcan2d  7982  pnncand  7983  ppncand  7984  subcand  7985  subcan2d  7986  subcanad  7987  subcan2ad  7989  subdid  8043  subdird  8044  ltadd2  8048  ltadd2d  8050  ltletrd  8052  ltsubadd  8061  lesubadd  8063  ltaddsub  8065  leaddsub  8067  le2add  8073  lt2add  8074  ltleadd  8075  lesub1  8085  lesub2  8086  ltsub1  8087  ltsub2  8088  lt2sub  8089  le2sub  8090  subge0  8104  lesub0  8108  ltadd1d  8166  leadd1d  8167  leadd2d  8168  ltsubaddd  8169  lesubaddd  8170  ltsubadd2d  8171  lesubadd2d  8172  ltaddsubd  8173  ltaddsub2d  8174  leaddsub2d  8175  subled  8176  lesubd  8177  ltsub23d  8178  ltsub13d  8179  lesub1d  8180  lesub2d  8181  ltsub1d  8182  ltsub2d  8183  gt0add  8201  apcotr  8235  apadd1  8236  addext  8238  mulext1  8240  mulext  8242  gtapd  8264  leltapd  8266  subap0d  8271  mulap0  8276  mul0eqap  8292  divvalap  8295  divcanap2  8301  diveqap0  8303  divrecap  8309  divassap  8311  divmulassap  8316  divmulasscomap  8317  divdirap  8318  divcanap3  8319  div11ap  8321  rec11ap  8331  divmuldivap  8333  divdivdivap  8334  divmuleqap  8338  dmdcanap  8343  ddcanap  8347  divadddivap  8348  divsubdivap  8349  redivclap  8352  apmul1  8409  divclapd  8411  divcanap1d  8412  divcanap2d  8413  divrecapd  8414  divrecap2d  8415  divcanap3d  8416  divcanap4d  8417  diveqap0d  8418  diveqap1d  8419  diveqap1ad  8420  diveqap0ad  8421  divap0bd  8423  divnegapd  8424  divneg2apd  8425  div2negapd  8426  redivclapd  8455  div2subap  8457  ltmul12a  8476  lemul12b  8477  lt2mul2div  8495  ltdiv2  8503  ltdiv23  8508  avglt1  8810  avglt2  8811  lt2halvesd  8819  div4p1lem1div2  8825  zltp1le  8960  elz2  8974  zdivmul  8993  uztrn  9192  eluzsub  9205  uz3m2nn  9218  qaddcl  9277  cnref1o  9290  ltdiv2d  9354  lediv2d  9355  divlt1lt  9358  divle1le  9359  ledivge1le  9360  ltmulgt11d  9366  ltmulgt12d  9367  gt0divd  9368  ge0divd  9369  rpgecld  9370  ltmul1d  9372  ltmul2d  9373  lemul1d  9374  lemul2d  9375  ltdiv1d  9376  lediv1d  9377  ltmuldivd  9378  ltmuldiv2d  9379  lemuldivd  9380  lemuldiv2d  9381  ltdivmuld  9382  ltdivmul2d  9383  ledivmuld  9384  ledivmul2d  9385  ltdiv23d  9391  lediv23d  9392  addlelt  9396  xrltso  9423  xrlelttr  9430  xrlttrd  9433  xrlelttrd  9434  xrltletrd  9435  xrletrd  9436  xrre3  9446  xleadd1  9499  xltadd1  9500  xle2add  9503  xlt2add  9504  xlesubadd  9507  xadd4d  9509  ixxss1  9528  ixxss2  9529  ixxss12  9530  iooshf  9576  icoshftf1o  9615  ioodisj  9617  zltaddlt1le  9630  fznlem  9662  fzdifsuc  9702  fzrev  9705  fzrevral2  9727  elfz0fzfz0  9744  elfzmlbp  9750  fzctr  9751  elfzole1  9773  elfzolt2  9774  fzoss2  9790  fzospliti  9794  fzo1fzo0n0  9801  elfzo0z  9802  fzofzim  9806  fzoaddel  9810  eluzgtdifelfzo  9815  elfzodifsumelfzo  9819  ssfzo12bi  9843  elfzonelfzo  9848  fvinim0ffz  9859  rebtwn2zlemstep  9871  rebtwn2z  9873  qbtwnxr  9876  flqge  9896  2tnp1ge0ge0  9915  intfracq  9934  flqdiv  9935  modqval  9938  modqcld  9942  modqmulnn  9956  zmodcl  9958  zmodfz  9960  modqid  9963  zmodid2  9966  modqabs  9971  modqcyc  9973  modqadd1  9975  modqaddabs  9976  modqaddmod  9977  mulp1mod1  9979  modqmuladd  9980  modqmuladdim  9981  modqmuladdnn0  9982  m1modnnsub1  9984  modqltm1p1mod  9990  modqmul1  9991  modqsubmod  9996  modqsubmodmod  9997  q2txmodxeq0  9998  modaddmodup  10001  modqmulmod  10003  modqaddmulmod  10005  modqdi  10006  modqsubdir  10007  addmodlteq  10012  frecuzrdgrrn  10022  frec2uzrdg  10023  frecuzrdgrcl  10024  frecuzrdgsuc  10028  frecuzrdgrclt  10029  frecuzrdgg  10030  frecuzrdgsuctlem  10037  frecfzen2  10041  seq3val  10072  seqvalcd  10073  seqf  10075  seq3p1  10076  seqovcd  10077  seqp1cd  10080  monoord  10090  iseqf1olemqcl  10100  iseqf1olemnab  10102  iseqf1olemmo  10106  iseqf1olemqk  10108  seq3f1olemqsumkj  10112  seq3f1olemstep  10115  expnnval  10137  expnegap0  10142  rpexpcl  10153  expnegzap  10168  expgt1  10172  mulexpzap  10174  exprecap  10175  expaddzaplem  10177  expaddzap  10178  expmul  10179  expmulzap  10180  expdivap  10185  ltexp2a  10186  leexp2a  10187  leexp2r  10188  leexp1a  10189  bernneq2  10254  bernneq3  10255  expnbnd  10256  expnlbnd  10257  expnlbnd2  10258  expaddd  10267  expmuld  10268  expclzapd  10270  expap0d  10271  expnegapd  10272  exprecapd  10273  expp1zapd  10274  expm1apd  10275  sqdivapd  10278  mulexpd  10280  expge0d  10283  expge1d  10284  sqoddm1div8  10285  reexpclzapd  10290  leexp2ad  10294  facwordi  10327  faclbnd3  10330  facavg  10333  bcval  10336  bccmpl  10341  bc0k  10343  bcval5  10350  bcpasc  10353  hashfiv01gt1  10369  hashunlem  10391  hashunsng  10394  fiprsshashgt1  10404  hashdifsn  10406  hashdifpr  10407  hashfz  10408  hashxp  10413  hashfacen  10420  zfz1isolemiso  10423  zfz1isolem1  10424  zfz1iso  10425  shftfvalg  10431  seq3shft  10451  mulreap  10477  cjreb  10479  cjap  10519  cnrecnv  10523  cjdivapd  10581  redivapd  10587  imdivapd  10588  resqrexlemdecn  10624  absexpzap  10692  abslt  10700  absle  10701  elicc4abs  10706  abs3lem  10723  fzomaxdiflem  10724  cau3lem  10726  amgm2  10730  abssubge0d  10788  abssuble0d  10789  absdifltd  10790  absdifled  10791  absdivapd  10807  abs3difd  10812  qdenre  10814  maxabslemlub  10819  rexanre  10832  rexico  10833  fimaxre2  10837  lemininf  10844  ltmininf  10845  rpmincl  10848  mul0inf  10851  xrmaxiflemlub  10856  xrmaxltsup  10866  xrmaxaddlem  10868  xrmaxadd  10869  xrltmininf  10878  xrlemininf  10879  xrminltinf  10880  xrminadd  10883  xrbdtri  10884  climshftlemg  10910  climshft2  10914  addcn2  10918  mulcn2  10920  reccn2ap  10921  cn1lem  10922  climadd  10934  climmul  10935  climsub  10936  climsqz  10943  climsqz2  10944  climrecvg1n  10956  climcvg1nlem  10957  fisumss  11000  fsumsplitsn  11018  sumpr  11021  fsumsplitsnun  11027  fsum2dlemstep  11042  fisumcom2  11046  fisum0diag2  11055  fsumconst  11062  modfsummodlemstep  11065  fsumlessfi  11068  fsumabs  11073  fsumiun  11085  hashiun  11086  hash2iun  11087  hash2iun1dif1  11088  binomlem  11091  bcxmas  11097  isumshft  11098  isumlessdc  11104  expcnvap0  11110  expcnvre  11111  geosergap  11114  cvgratnnlembern  11131  cvgratnnlemnexp  11132  cvgratnnlemmn  11133  mertenslemi1  11143  efaddlem  11178  eftlub  11194  efltim  11202  eirraplem  11278  dvdsval3  11292  nndivdvds  11294  summodnegmod  11319  modmulconst  11320  dvds2subd  11324  dvdsmultr1d  11327  dvdsmultr2  11328  dvdsabseq  11340  dvdsfac  11353  dvdsmod  11355  oddge22np1  11373  ltoddhalfle  11385  halfleoddlt  11386  nn0ehalf  11395  nno  11398  nn0oddm1d2  11401  divalglemnn  11410  divalg  11416  divalgmod  11419  fldivndvdslt  11427  flodddiv4lt  11428  flodddiv4t2lthalf  11429  infssuzex  11437  dvdsbnd  11440  gcdneg  11465  gcdaddm  11467  modgcd  11474  bezoutlemnewy  11477  bezoutlemstep  11478  bezoutlembi  11486  dvdsgcdb  11494  gcdass  11496  mulgcd  11497  dvdsmulgcd  11506  rpmulgcd  11507  sqgcd  11510  nn0seqcvgd  11515  eucalglt  11531  gcddvdslcm  11547  lcmgcdlem  11551  lcmdvdsb  11558  lcmass  11559  ncoprmgcdne1b  11563  coprmdvds2  11567  mulgcddvds  11568  rpmulgcd2  11569  qredeu  11571  rpdvds  11573  divgcdcoprm0  11575  cncongr1  11577  cncongr2  11578  isprm2lem  11590  prmind2  11594  nprm  11597  dvdsnprmd  11599  exprmfct  11611  prmdvdsfz  11612  divgcdodd  11614  isprm6  11618  prmdvdsexp  11619  prmexpb  11622  prmfac1  11623  rpexp  11624  rpexp12i  11626  pw2dvdseulemle  11637  sqpweven  11645  2sqpwodd  11646  divnumden  11666  numdensq  11672  nonsq  11677  hashdvds  11689  phiprmpw  11690  crth  11692  phimullem  11693  hashgcdlem  11695  ennnfonelemp1  11711  ennnfonelemex  11719  ennnfonelemrn  11724  ctinfom  11733  strsetsid  11774  fvsetsid  11775  setsabsd  11780  setscom  11781  ressid2  11800  ressval2  11801  srngstrd  11863  lmodstrd  11874  ipsstrd  11882  topgrpstrd  11892  difopn  12059  uncld  12064  ntrin  12075  clsss2  12080  ntrcls0  12082  topssnei  12113  neissex  12116  restbasg  12119  tgrest  12120  resttopon  12122  restabs  12126  restopnb  12132  cnpfval  12146  cnprcl2k  12156  tgcnp  12159  iscnp4  12168  cnpnei  12169  cnptopco  12172  cncnpi  12178  cncnp  12180  cnconst2  12183  cnrest  12185  cnrest2  12186  cnrest2r  12187  cnptopresti  12188  cnptoprest  12189  cnptoprest2  12190  lmss  12196  lmtopcnp  12200  txvalex  12204  txval  12205  txbasval  12217  txcnp  12221  txcnmpt  12223  txcn  12225  txdis1cn  12228  lmcn2  12230  cnmptc  12232  cnmpt11  12233  cnmpt1t  12235  cnmpt12  12237  cnmpt21  12241  cnmpt2t  12243  cnmpt22  12244  cnmpt22f  12245  cnmptcom  12248  psmettri  12258  xmettri  12300  metrtri  12305  xmetres2  12307  blfvalps  12313  bldisj  12329  blgt0  12330  xblss2ps  12332  xblss2  12333  blhalf  12336  blininf  12352  blssps  12355  blss  12356  blssexps  12357  blssex  12358  blin2  12360  xmeter  12364  blnei  12420  blsscls2  12421  metss2lem  12425  bdmetval  12428  bdxmet  12429  bdbl  12431  metcnp3  12435  metcnp  12436  metcnp2  12437  metcnpi  12439  metcnpi2  12440  metcnpi3  12441  metcnpd  12442  tgqioo  12466  mulc1cncf  12489  cncfco  12491  mulcncflem  12502  mulcncf  12503  limccl  12510  ellimc3ap  12511  limcimolemlt  12513  limccnpcntop  12520  reldvg  12521  eldvap  12524  dvbssntrcntop  12526