Theorem syl3anc 1172

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 1121	. 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 922

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 924

This theorem is referenced by:  syl112anc  1176  syl121anc  1177  syl211anc  1178  syl113anc  1184  syl131anc  1185  syl311anc  1186  syld3an3  1217  3jaod  1238  mpd3an23  1273  stoic4a  1364  rspc3ev  2730  sbciedf  2863  euotd  4054  ordelord  4181  wetriext  4364  releldm  4637  relelrn  4638  f1imass  5508  ovmpt2dxf  5721  ovmpt2df  5727  fovrnd  5740  offval  5814  fnofval  5816  caoftrn  5831  offval3  5856  tfrlemisucaccv  6038  tfrlemiubacc  6043  tfr1onlemsucaccv  6054  tfr1onlembfn  6057  tfrcllemsucaccv  6067  tfrcllembfn  6070  rdgss  6096  rdgisuc1  6097  rdgisucinc  6098  frecrdg  6121  mapsspm  6385  en2d  6431  en3d  6432  dom3d  6437  ssdomg  6441  f1imaen2g  6456  2dom  6468  cnven  6471  mapen  6508  mapxpen  6510  phpelm  6528  fidifsnen  6532  dif1en  6541  dif1enen  6542  diffisn  6555  isinfinf  6559  unfidisj  6578  unfiin  6582  xpfi  6584  fisseneq  6586  ssfirab  6587  fnfi  6590  f1dmvrnfibi  6597  f1finf1o  6599  en1eqsn  6600  updjudhcoinlf  6708  updjudhcoinrg  6709  en2eleq  6758  en2other2  6759  addcmpblnq  6863  addassnqg  6878  distrnqg  6883  ltsonq  6894  ltanqg  6896  ltmnqg  6897  ltaddnq  6903  ltexnqq  6904  prarloclemarch  6914  ltrnqg  6916  addcmpblnq0  6939  nnanq0  6954  distrnq0  6955  addassnq0  6958  prarloclemlt  6989  prarloclemcalc  6998  addnqprllem  7023  addnqprulem  7024  addnqprl  7025  addnqpru  7026  addlocprlemgt  7030  appdivnq  7059  prmuloclemcalc  7061  mulnqprl  7064  mulnqpru  7065  mullocprlem  7066  distrlem4prl  7080  distrlem4pru  7081  ltprordil  7085  ltexprlemopl  7097  ltexprlemopu  7099  ltexprlemloc  7103  ltexprlemru  7108  addcanprleml  7110  addcanprlemu  7111  ltaprlem  7114  ltaprg  7115  addextpr  7117  recexprlem1ssu  7130  aptipr  7137  ltmprr  7138  caucvgprlemcanl  7140  cauappcvgprlemopl  7142  cauappcvgprlemdisj  7147  cauappcvgprlemloc  7148  cauappcvgprlemladdfu  7150  cauappcvgprlemladdru  7152  cauappcvgprlemladdrl  7153  cauappcvgprlem1  7155  caucvgprlemm  7164  caucvgprlemopl  7165  caucvgprlemloc  7171  caucvgprlemladdfu  7173  caucvgprlemladdrl  7174  caucvgprprlemloccalc  7180  caucvgprprlemml  7190  caucvgprprlemopl  7193  caucvgprprlemloc  7199  caucvgprprlemexb  7203  caucvgprprlemaddq  7204  caucvgprprlem1  7205  caucvgprprlem2  7206  addcmpblnr  7222  mulcmpblnrlemg  7223  mulcmpblnr  7224  ltsrprg  7230  distrsrg  7242  lttrsr  7245  ltsosr  7247  1idsr  7251  ltasrg  7253  recexgt0sr  7256  mulgt0sr  7260  mulextsr1lem  7262  srpospr  7265  prsradd  7268  prsrlt  7269  caucvgsrlemoffval  7278  caucvgsrlemoffgt1  7281  caucvgsrlemoffres  7282  caucvgsr  7284  pitoregt0  7323  recidpirqlemcalc  7331  axmulass  7345  axdistr  7346  rereceu  7361  recriota  7362  addassd  7447  mulassd  7448  adddid  7449  adddird  7450  lelttr  7510  letrd  7544  lelttrd  7545  lttrd  7546  mul12d  7571  mul32d  7572  mul31d  7573  add12d  7586  add32d  7587  cnegexlem3  7596  addcand  7603  addcan2d  7604  pncan  7625  pncan3  7627  subcan2  7644  subsub2  7647  subsub4  7652  npncan3  7657  pnpcan  7658  pnncan  7660  addsub4  7662  subaddd  7748  subadd2d  7749  addsubassd  7750  addsubd  7751  subadd23d  7752  addsub12d  7753  npncand  7754  nppcand  7755  nppcan2d  7756  nppcan3d  7757  subsubd  7758  subsub2d  7759  subsub3d  7760  subsub4d  7761  sub32d  7762  nnncand  7763  nnncan1d  7764  nnncan2d  7765  npncan3d  7766  pnpcand  7767  pnpcan2d  7768  pnncand  7769  ppncand  7770  subcand  7771  subcan2d  7772  subcanad  7773  subcan2ad  7775  subdid  7829  subdird  7830  ltadd2  7834  ltadd2d  7836  ltletrd  7838  ltsubadd  7847  lesubadd  7849  ltaddsub  7851  leaddsub  7853  le2add  7859  lt2add  7860  ltleadd  7861  lesub1  7871  lesub2  7872  ltsub1  7873  ltsub2  7874  lt2sub  7875  le2sub  7876  subge0  7890  lesub0  7894  ltadd1d  7949  leadd1d  7950  leadd2d  7951  ltsubaddd  7952  lesubaddd  7953  ltsubadd2d  7954  lesubadd2d  7955  ltaddsubd  7956  ltaddsub2d  7957  leaddsub2d  7958  subled  7959  lesubd  7960  ltsub23d  7961  ltsub13d  7962  lesub1d  7963  lesub2d  7964  ltsub1d  7965  ltsub2d  7966  gt0add  7984  apcotr  8018  apadd1  8019  addext  8021  mulext1  8023  mulext  8025  gtapd  8046  leltapd  8048  subap0d  8051  mulap0  8055  divvalap  8073  divcanap2  8079  diveqap0  8081  divrecap  8087  divassap  8089  divmulassap  8094  divmulasscomap  8095  divdirap  8096  divcanap3  8097  div11ap  8099  rec11ap  8109  divmuldivap  8111  divdivdivap  8112  divmuleqap  8116  dmdcanap  8121  ddcanap  8125  divadddivap  8126  divsubdivap  8127  redivclap  8130  apmul1  8187  divclapd  8188  divcanap1d  8189  divcanap2d  8190  divrecapd  8191  divrecap2d  8192  divcanap3d  8193  divcanap4d  8194  diveqap0d  8195  diveqap1d  8196  diveqap1ad  8197  diveqap0ad  8198  divap0bd  8200  divnegapd  8201  divneg2apd  8202  div2negapd  8203  redivclapd  8231  ltmul12a  8249  lemul12b  8250  lt2mul2div  8268  ltdiv2  8276  ltdiv23  8281  avglt1  8580  avglt2  8581  lt2halvesd  8589  div4p1lem1div2  8595  zltp1le  8730  elz2  8744  zdivmul  8762  uztrn  8960  eluzsub  8973  uz3m2nn  8986  qaddcl  9045  cnref1o  9058  ltdiv2d  9122  lediv2d  9123  divlt1lt  9126  divle1le  9127  ledivge1le  9128  ltmulgt11d  9134  ltmulgt12d  9135  gt0divd  9136  ge0divd  9137  rpgecld  9138  ltmul1d  9140  ltmul2d  9141  lemul1d  9142  lemul2d  9143  ltdiv1d  9144  lediv1d  9145  ltmuldivd  9146  ltmuldiv2d  9147  lemuldivd  9148  lemuldiv2d  9149  ltdivmuld  9150  ltdivmul2d  9151  ledivmuld  9152  ledivmul2d  9153  ltdiv23d  9159  lediv23d  9160  addlelt  9164  xrltso  9191  xrlelttr  9196  xrlttrd  9199  xrlelttrd  9200  xrltletrd  9201  xrletrd  9202  xrre3  9209  ixxss1  9247  ixxss2  9248  ixxss12  9249  iooshf  9295  icoshftf1o  9333  ioodisj  9335  zltaddlt1le  9348  fznlem  9380  fzdifsuc  9418  fzrev  9421  fzrevral2  9443  elfz0fzfz0  9458  elfzmlbp  9464  fzctr  9465  elfzole1  9487  elfzolt2  9488  fzoss2  9504  fzospliti  9508  fzo1fzo0n0  9515  elfzo0z  9516  fzofzim  9520  fzoaddel  9524  eluzgtdifelfzo  9529  elfzodifsumelfzo  9533  ssfzo12bi  9557  elfzonelfzo  9562  fvinim0ffz  9573  rebtwn2zlemstep  9585  rebtwn2z  9587  qbtwnxr  9590  flqge  9610  2tnp1ge0ge0  9629  intfracq  9648  flqdiv  9649  modqval  9652  modqcld  9656  modqmulnn  9670  zmodcl  9672  zmodfz  9674  modqid  9677  zmodid2  9680  modqabs  9685  modqcyc  9687  modqadd1  9689  modqaddabs  9690  modqaddmod  9691  mulp1mod1  9693  modqmuladd  9694  modqmuladdim  9695  modqmuladdnn0  9696  m1modnnsub1  9698  modqltm1p1mod  9704  modqmul1  9705  modqsubmod  9710  modqsubmodmod  9711  q2txmodxeq0  9712  modaddmodup  9715  modqmulmod  9717  modqaddmulmod  9719  modqdi  9720  modqsubdir  9721  addmodlteq  9726  frecuzrdgrrn  9736  frec2uzrdg  9737  frecuzrdgrcl  9738  frecuzrdgsuc  9742  frecuzrdgrclt  9743  frecuzrdgg  9744  frecuzrdgsuctlem  9751  frecfzen2  9755  iseqval  9781  iseqvalt  9783  iseqfclt  9787  iseqp1  9789  iseqp1t  9790  monoord  9802  iseqf1olemqcl  9812  iseqf1olemnab  9814  iseqf1olemmo  9818  iseqf1olemqk  9820  iseqf1olemqsumkj  9824  iseqf1olemstep  9827  expinnval  9849  expnegap0  9854  rpexpcl  9865  expnegzap  9880  expgt1  9884  mulexpzap  9886  exprecap  9887  expaddzaplem  9889  expaddzap  9890  expmul  9891  expmulzap  9892  expdivap  9897  ltexp2a  9898  leexp2a  9899  leexp2r  9900  leexp1a  9901  bernneq2  9964  bernneq3  9965  expnbnd  9966  expnlbnd  9967  expnlbnd2  9968  expaddd  9977  expmuld  9978  expclzapd  9980  expap0d  9981  expnegapd  9982  exprecapd  9983  expp1zapd  9984  expm1apd  9985  sqdivapd  9988  mulexpd  9990  expge0d  9993  expge1d  9994  sqoddm1div8  9995  reexpclzapd  10000  leexp2ad  10004  facwordi  10037  faclbnd3  10040  facavg  10043  bcval  10046  bccmpl  10051  bc0k  10053  ibcval5  10060  bcpasc  10063  hashfiv01gt1  10079  hashunlem  10101  hashunsng  10104  fiprsshashgt1  10114  hashdifsn  10116  hashdifpr  10117  hashfz  10118  hashxp  10123  hashfacen  10130  zfz1isolemiso  10133  zfz1isolem1  10134  zfz1iso  10135  shftfvalg  10141  mulreap  10186  cjreb  10188  cjap  10228  cnrecnv  10232  cjdivapd  10290  redivapd  10296  imdivapd  10297  resqrexlemdecn  10333  absexpzap  10401  abslt  10409  absle  10410  elicc4abs  10415  abs3lem  10432  fzomaxdiflem  10433  cau3lem  10435  amgm2  10439  abssubge0d  10497  abssuble0d  10498  absdifltd  10499  absdifled  10500  absdivapd  10516  abs3difd  10521  qdenre  10523  maxabslemlub  10528  rexanre  10541  rexico  10542  fimaxre2  10544  lemininf  10550  ltmininf  10551  climshftlemg  10576  climshft2  10580  addcn2  10584  mulcn2  10586  cn1lem  10587  climadd  10599  climmul  10600  climsub  10601  climsqz  10608  climsqz2  10609  climrecvg1n  10620  climcvg1nlem  10621  dvdsval3  10667  nndivdvds  10669  summodnegmod  10694  modmulconst  10695  dvds2subd  10699  dvdsmultr1d  10702  dvdsmultr2  10703  dvdsabseq  10715  dvdsfac  10728  dvdsmod  10730  oddge22np1  10748  ltoddhalfle  10760  halfleoddlt  10761  nn0ehalf  10770  nno  10773  nn0oddm1d2  10776  divalglemnn  10785  divalg  10791  divalgmod  10794  fldivndvdslt  10802  flodddiv4lt  10803  flodddiv4t2lthalf  10804  infssuzex  10812  dvdsbnd  10815  gcdneg  10840  gcdaddm  10842  modgcd  10849  bezoutlemnewy  10852  bezoutlemstep  10853  bezoutlembi  10861  dvdsgcdb  10869  gcdass  10871  mulgcd  10872  dvdsmulgcd  10881  rpmulgcd  10882  sqgcd  10885  nn0seqcvgd  10890  eucalglt  10906  gcddvdslcm  10922  lcmgcdlem  10926  lcmdvdsb  10933  lcmass  10934  ncoprmgcdne1b  10938  coprmdvds2  10942  mulgcddvds  10943  rpmulgcd2  10944  qredeu  10946  rpdvds  10948  divgcdcoprm0  10950  cncongr1  10952  cncongr2  10953  isprm2lem  10965  prmind2  10969  nprm  10972  dvdsnprmd  10974  exprmfct  10986  prmdvdsfz  10987  divgcdodd  10989  isprm6  10993  prmdvdsexp  10994  prmexpb  10997  prmfac1  10998  rpexp  10999  rpexp12i  11001  pw2dvdseulemle  11012  sqpweven  11020  2sqpwodd  11021  divnumden  11041  numdensq  11047  nonsq  11052  hashdvds  11064  phiprmpw  11065  crth  11067  phimullem  11068  hashgcdlem  11070