Theorem syl3anc 1170

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 1119	. 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 920

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

This theorem depends on definitions:  df-bi 115  df-3an 922

This theorem is referenced by:  syl112anc  1174  syl121anc  1175  syl211anc  1176  syl113anc  1182  syl131anc  1183  syl311anc  1184  syld3an3  1215  3jaod  1236  mpd3an23  1271  stoic4a  1362  rspc3ev  2727  sbciedf  2860  euotd  4045  ordelord  4172  wetriext  4355  releldm  4628  relelrn  4629  f1imass  5493  ovmpt2dxf  5705  ovmpt2df  5711  fovrnd  5724  offval  5798  fnofval  5800  caoftrn  5815  offval3  5840  tfrlemisucaccv  6022  tfrlemiubacc  6027  tfr1onlemsucaccv  6038  tfr1onlembfn  6041  tfrcllemsucaccv  6051  tfrcllembfn  6054  rdgss  6080  rdgisuc1  6081  rdgisucinc  6082  frecrdg  6105  mapsspm  6369  en2d  6415  en3d  6416  dom3d  6421  ssdomg  6425  f1imaen2g  6440  2dom  6452  cnven  6455  mapen  6492  mapxpen  6494  phpelm  6512  fidifsnen  6516  dif1en  6525  dif1enen  6526  diffisn  6539  isinfinf  6543  unfidisj  6559  unfiin  6563  xpfi  6565  fisseneq  6567  ssfirab  6568  fnfi  6571  f1dmvrnfibi  6578  f1finf1o  6580  en1eqsn  6581  updjudhcoinlf  6678  updjudhcoinrg  6679  en2eleq  6724  en2other2  6725  addcmpblnq  6829  addassnqg  6844  distrnqg  6849  ltsonq  6860  ltanqg  6862  ltmnqg  6863  ltaddnq  6869  ltexnqq  6870  prarloclemarch  6880  ltrnqg  6882  addcmpblnq0  6905  nnanq0  6920  distrnq0  6921  addassnq0  6924  prarloclemlt  6955  prarloclemcalc  6964  addnqprllem  6989  addnqprulem  6990  addnqprl  6991  addnqpru  6992  addlocprlemgt  6996  appdivnq  7025  prmuloclemcalc  7027  mulnqprl  7030  mulnqpru  7031  mullocprlem  7032  distrlem4prl  7046  distrlem4pru  7047  ltprordil  7051  ltexprlemopl  7063  ltexprlemopu  7065  ltexprlemloc  7069  ltexprlemru  7074  addcanprleml  7076  addcanprlemu  7077  ltaprlem  7080  ltaprg  7081  addextpr  7083  recexprlem1ssu  7096  aptipr  7103  ltmprr  7104  caucvgprlemcanl  7106  cauappcvgprlemopl  7108  cauappcvgprlemdisj  7113  cauappcvgprlemloc  7114  cauappcvgprlemladdfu  7116  cauappcvgprlemladdru  7118  cauappcvgprlemladdrl  7119  cauappcvgprlem1  7121  caucvgprlemm  7130  caucvgprlemopl  7131  caucvgprlemloc  7137  caucvgprlemladdfu  7139  caucvgprlemladdrl  7140  caucvgprprlemloccalc  7146  caucvgprprlemml  7156  caucvgprprlemopl  7159  caucvgprprlemloc  7165  caucvgprprlemexb  7169  caucvgprprlemaddq  7170  caucvgprprlem1  7171  caucvgprprlem2  7172  addcmpblnr  7188  mulcmpblnrlemg  7189  mulcmpblnr  7190  ltsrprg  7196  distrsrg  7208  lttrsr  7211  ltsosr  7213  1idsr  7217  ltasrg  7219  recexgt0sr  7222  mulgt0sr  7226  mulextsr1lem  7228  srpospr  7231  prsradd  7234  prsrlt  7235  caucvgsrlemoffval  7244  caucvgsrlemoffgt1  7247  caucvgsrlemoffres  7248  caucvgsr  7250  pitoregt0  7289  recidpirqlemcalc  7297  axmulass  7311  axdistr  7312  rereceu  7327  recriota  7328  addassd  7413  mulassd  7414  adddid  7415  adddird  7416  lelttr  7476  letrd  7510  lelttrd  7511  lttrd  7512  mul12d  7537  mul32d  7538  mul31d  7539  add12d  7552  add32d  7553  cnegexlem3  7562  addcand  7569  addcan2d  7570  pncan  7591  pncan3  7593  subcan2  7610  subsub2  7613  subsub4  7618  npncan3  7623  pnpcan  7624  pnncan  7626  addsub4  7628  subaddd  7714  subadd2d  7715  addsubassd  7716  addsubd  7717  subadd23d  7718  addsub12d  7719  npncand  7720  nppcand  7721  nppcan2d  7722  nppcan3d  7723  subsubd  7724  subsub2d  7725  subsub3d  7726  subsub4d  7727  sub32d  7728  nnncand  7729  nnncan1d  7730  nnncan2d  7731  npncan3d  7732  pnpcand  7733  pnpcan2d  7734  pnncand  7735  ppncand  7736  subcand  7737  subcan2d  7738  subcanad  7739  subcan2ad  7741  subdid  7795  subdird  7796  ltadd2  7800  ltadd2d  7802  ltletrd  7804  ltsubadd  7813  lesubadd  7815  ltaddsub  7817  leaddsub  7819  le2add  7825  lt2add  7826  ltleadd  7827  lesub1  7837  lesub2  7838  ltsub1  7839  ltsub2  7840  lt2sub  7841  le2sub  7842  subge0  7856  lesub0  7860  ltadd1d  7915  leadd1d  7916  leadd2d  7917  ltsubaddd  7918  lesubaddd  7919  ltsubadd2d  7920  lesubadd2d  7921  ltaddsubd  7922  ltaddsub2d  7923  leaddsub2d  7924  subled  7925  lesubd  7926  ltsub23d  7927  ltsub13d  7928  lesub1d  7929  lesub2d  7930  ltsub1d  7931  ltsub2d  7932  gt0add  7950  apcotr  7984  apadd1  7985  addext  7987  mulext1  7989  mulext  7991  gtapd  8012  leltapd  8014  subap0d  8017  mulap0  8021  divvalap  8039  divcanap2  8045  diveqap0  8047  divrecap  8053  divassap  8055  divmulassap  8060  divmulasscomap  8061  divdirap  8062  divcanap3  8063  div11ap  8065  rec11ap  8075  divmuldivap  8077  divdivdivap  8078  divmuleqap  8082  dmdcanap  8087  ddcanap  8091  divadddivap  8092  divsubdivap  8093  redivclap  8096  apmul1  8153  divclapd  8154  divcanap1d  8155  divcanap2d  8156  divrecapd  8157  divrecap2d  8158  divcanap3d  8159  divcanap4d  8160  diveqap0d  8161  diveqap1d  8162  diveqap1ad  8163  diveqap0ad  8164  divap0bd  8166  divnegapd  8167  divneg2apd  8168  div2negapd  8169  redivclapd  8197  ltmul12a  8215  lemul12b  8216  lt2mul2div  8234  ltdiv2  8242  ltdiv23  8247  avglt1  8546  avglt2  8547  lt2halvesd  8555  div4p1lem1div2  8561  zltp1le  8700  elz2  8714  zdivmul  8732  uztrn  8930  eluzsub  8943  uz3m2nn  8956  qaddcl  9015  cnref1o  9028  ltdiv2d  9092  lediv2d  9093  divlt1lt  9096  divle1le  9097  ledivge1le  9098  ltmulgt11d  9104  ltmulgt12d  9105  gt0divd  9106  ge0divd  9107  rpgecld  9108  ltmul1d  9110  ltmul2d  9111  lemul1d  9112  lemul2d  9113  ltdiv1d  9114  lediv1d  9115  ltmuldivd  9116  ltmuldiv2d  9117  lemuldivd  9118  lemuldiv2d  9119  ltdivmuld  9120  ltdivmul2d  9121  ledivmuld  9122  ledivmul2d  9123  ltdiv23d  9129  lediv23d  9130  addlelt  9134  xrltso  9161  xrlelttr  9166  xrlttrd  9169  xrlelttrd  9170  xrltletrd  9171  xrletrd  9172  xrre3  9179  ixxss1  9217  ixxss2  9218  ixxss12  9219  iooshf  9265  icoshftf1o  9303  ioodisj  9305  zltaddlt1le  9318  fznlem  9350  fzdifsuc  9388  fzrev  9391  fzrevral2  9413  elfz0fzfz0  9428  elfzmlbp  9434  fzctr  9435  elfzole1  9455  elfzolt2  9456  fzoss2  9472  fzospliti  9476  fzo1fzo0n0  9483  elfzo0z  9484  fzofzim  9488  fzoaddel  9492  eluzgtdifelfzo  9497  elfzodifsumelfzo  9501  ssfzo12bi  9525  elfzonelfzo  9530  fvinim0ffz  9541  rebtwn2zlemstep  9553  rebtwn2z  9555  qbtwnxr  9558  flqge  9578  2tnp1ge0ge0  9597  intfracq  9616  flqdiv  9617  modqval  9620  modqcld  9624  modqmulnn  9638  zmodcl  9640  zmodfz  9642  modqid  9645  zmodid2  9648  modqabs  9653  modqcyc  9655  modqadd1  9657  modqaddabs  9658  modqaddmod  9659  mulp1mod1  9661  modqmuladd  9662  modqmuladdim  9663  modqmuladdnn0  9664  m1modnnsub1  9666  modqltm1p1mod  9672  modqmul1  9673  modqsubmod  9678  modqsubmodmod  9679  q2txmodxeq0  9680  modaddmodup  9683  modqmulmod  9685  modqaddmulmod  9687  modqdi  9688  modqsubdir  9689  addmodlteq  9694  frecuzrdgrrn  9704  frec2uzrdg  9705  frecuzrdgrcl  9706  frecuzrdgsuc  9710  frecuzrdgrclt  9711  frecuzrdgg  9712  frecuzrdgsuctlem  9719  frecfzen2  9723  iseqval  9749  iseqvalt  9751  iseqfclt  9755  iseqp1  9757  iseqp1t  9758  monoord  9770  expinnval  9795  expnegap0  9800  rpexpcl  9811  expnegzap  9826  expgt1  9830  mulexpzap  9832  exprecap  9833  expaddzaplem  9835  expaddzap  9836  expmul  9837  expmulzap  9838  expdivap  9843  ltexp2a  9844  leexp2a  9845  leexp2r  9846  leexp1a  9847  bernneq2  9910  bernneq3  9911  expnbnd  9912  expnlbnd  9913  expnlbnd2  9914  expaddd  9923  expmuld  9924  expclzapd  9926  expap0d  9927  expnegapd  9928  exprecapd  9929  expp1zapd  9930  expm1apd  9931  sqdivapd  9934  mulexpd  9936  expge0d  9939  expge1d  9940  sqoddm1div8  9941  reexpclzapd  9946  leexp2ad  9950  facwordi  9983  faclbnd3  9986  facavg  9989  bcval  9992  bccmpl  9997  bc0k  9999  ibcval5  10006  bcpasc  10009  hashfiv01gt1  10025  hashunlem  10047  hashunsng  10050  fiprsshashgt1  10060  hashdifsn  10062  hashdifpr  10063  hashfz  10064  hashxp  10069  hashfacen  10075  shftfvalg  10080  mulreap  10125  cjreb  10127  cjap  10167  cnrecnv  10171  cjdivapd  10229  redivapd  10235  imdivapd  10236  resqrexlemdecn  10272  absexpzap  10340  abslt  10348  absle  10349  elicc4abs  10354  abs3lem  10371  fzomaxdiflem  10372  cau3lem  10374  amgm2  10378  abssubge0d  10436  abssuble0d  10437  absdifltd  10438  absdifled  10439  absdivapd  10455  abs3difd  10460  qdenre  10462  maxabslemlub  10467  rexanre  10480  rexico  10481  fimaxre2  10483  lemininf  10489  ltmininf  10490  climshftlemg  10515  climshft2  10519  addcn2  10523  mulcn2  10525  cn1lem  10526  climadd  10538  climmul  10539  climsub  10540  climsqz  10547  climsqz2  10548  climrecvg1n  10559  climcvg1nlem  10560  dvdsval3  10580  nndivdvds  10582  summodnegmod  10607  modmulconst  10608  dvds2subd  10612  dvdsmultr1d  10615  dvdsmultr2  10616  dvdsabseq  10628  dvdsfac  10641  dvdsmod  10643  oddge22np1  10661  ltoddhalfle  10673  halfleoddlt  10674  nn0ehalf  10683  nno  10686  nn0oddm1d2  10689  divalglemnn  10698  divalg  10704  divalgmod  10707  fldivndvdslt  10715  flodddiv4lt  10716  flodddiv4t2lthalf  10717  infssuzex  10725  dvdsbnd  10728  gcdneg  10753  gcdaddm  10755  modgcd  10762  bezoutlemnewy  10765  bezoutlemstep  10766  bezoutlembi  10774  dvdsgcdb  10782  gcdass  10784  mulgcd  10785  dvdsmulgcd  10794  rpmulgcd  10795  sqgcd  10798  nn0seqcvgd  10803  eucalglt  10819  gcddvdslcm  10835  lcmgcdlem  10839  lcmdvdsb  10846  lcmass  10847  ncoprmgcdne1b  10851  coprmdvds2  10855  mulgcddvds  10856  rpmulgcd2  10857  qredeu  10859  rpdvds  10861  divgcdcoprm0  10863  cncongr1  10865  cncongr2  10866  isprm2lem  10878  prmind2  10882  nprm  10885  dvdsnprmd  10887  exprmfct  10899  prmdvdsfz  10900  divgcdodd  10902  isprm6  10906  prmdvdsexp  10907  prmexpb  10910  prmfac1  10911  rpexp  10912  rpexp12i  10914  pw2dvdseulemle  10925  sqpweven  10933  2sqpwodd  10934  divnumden  10954  numdensq  10960  nonsq  10965  hashdvds  10977  phiprmpw  10978  crth  10980  phimullem  10981  hashgcdlem  10983