Theorem syl3anc 1169

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 1118	. 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 919

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 921

This theorem is referenced by:  syl112anc  1173  syl121anc  1174  syl211anc  1175  syl113anc  1181  syl131anc  1182  syl311anc  1183  syld3an3  1214  3jaod  1235  mpd3an23  1270  stoic4a  1361  rspc3ev  2717  sbciedf  2849  euotd  4009  ordelord  4136  wetriext  4319  releldm  4587  relelrn  4588  f1imass  5434  ovmpt2dxf  5646  ovmpt2df  5652  fovrnd  5665  offval  5739  fnofval  5741  caoftrn  5756  offval3  5781  tfrlemisucaccv  5962  tfrlemiubacc  5967  rdgss  5993  rdgisuc1  5994  rdgisucinc  5995  freccl  6016  en2d  6271  en3d  6272  dom3d  6277  ssdomg  6281  f1imaen2g  6296  2dom  6308  cnven  6311  phpelm  6352  fidifsnen  6355  fidifsnid  6356  dif1en  6364  diffisn  6377  fnfi  6388  f1dmvrnfibi  6393  addcmpblnq  6557  addassnqg  6572  distrnqg  6577  ltsonq  6588  ltanqg  6590  ltmnqg  6591  ltaddnq  6597  ltexnqq  6598  prarloclemarch  6608  ltrnqg  6610  addcmpblnq0  6633  nnanq0  6648  distrnq0  6649  addassnq0  6652  prarloclemlt  6683  prarloclemcalc  6692  addnqprllem  6717  addnqprulem  6718  addnqprl  6719  addnqpru  6720  addlocprlemgt  6724  appdivnq  6753  prmuloclemcalc  6755  mulnqprl  6758  mulnqpru  6759  mullocprlem  6760  distrlem4prl  6774  distrlem4pru  6775  ltprordil  6779  ltexprlemopl  6791  ltexprlemopu  6793  ltexprlemloc  6797  ltexprlemru  6802  addcanprleml  6804  addcanprlemu  6805  ltaprlem  6808  ltaprg  6809  addextpr  6811  recexprlem1ssu  6824  aptipr  6831  ltmprr  6832  caucvgprlemcanl  6834  cauappcvgprlemopl  6836  cauappcvgprlemdisj  6841  cauappcvgprlemloc  6842  cauappcvgprlemladdfu  6844  cauappcvgprlemladdru  6846  cauappcvgprlemladdrl  6847  cauappcvgprlem1  6849  caucvgprlemm  6858  caucvgprlemopl  6859  caucvgprlemloc  6865  caucvgprlemladdfu  6867  caucvgprlemladdrl  6868  caucvgprprlemloccalc  6874  caucvgprprlemml  6884  caucvgprprlemopl  6887  caucvgprprlemloc  6893  caucvgprprlemexb  6897  caucvgprprlemaddq  6898  caucvgprprlem1  6899  caucvgprprlem2  6900  addcmpblnr  6916  mulcmpblnrlemg  6917  mulcmpblnr  6918  ltsrprg  6924  distrsrg  6936  lttrsr  6939  ltsosr  6941  1idsr  6945  ltasrg  6947  recexgt0sr  6950  mulgt0sr  6954  mulextsr1lem  6956  srpospr  6959  prsradd  6962  prsrlt  6963  caucvgsrlemoffval  6972  caucvgsrlemoffgt1  6975  caucvgsrlemoffres  6976  caucvgsr  6978  pitoregt0  7017  recidpirqlemcalc  7025  axmulass  7039  axdistr  7040  rereceu  7055  recriota  7056  addassd  7141  mulassd  7142  adddid  7143  adddird  7144  lelttr  7199  letrd  7233  lelttrd  7234  lttrd  7235  mul12d  7260  mul32d  7261  mul31d  7262  add12d  7275  add32d  7276  cnegexlem3  7285  addcand  7292  addcan2d  7293  pncan  7314  pncan3  7316  subcan2  7333  subsub2  7336  subsub4  7341  npncan3  7346  pnpcan  7347  pnncan  7349  addsub4  7351  subaddd  7437  subadd2d  7438  addsubassd  7439  addsubd  7440  subadd23d  7441  addsub12d  7442  npncand  7443  nppcand  7444  nppcan2d  7445  nppcan3d  7446  subsubd  7447  subsub2d  7448  subsub3d  7449  subsub4d  7450  sub32d  7451  nnncand  7452  nnncan1d  7453  nnncan2d  7454  npncan3d  7455  pnpcand  7456  pnpcan2d  7457  pnncand  7458  ppncand  7459  subcand  7460  subcan2d  7461  subcanad  7462  subcan2ad  7464  subdid  7518  subdird  7519  ltadd2  7523  ltadd2d  7525  ltletrd  7527  ltsubadd  7536  lesubadd  7538  ltaddsub  7540  leaddsub  7542  le2add  7548  lt2add  7549  ltleadd  7550  lesub1  7560  lesub2  7561  ltsub1  7562  ltsub2  7563  lt2sub  7564  le2sub  7565  subge0  7579  lesub0  7583  ltadd1d  7638  leadd1d  7639  leadd2d  7640  ltsubaddd  7641  lesubaddd  7642  ltsubadd2d  7643  lesubadd2d  7644  ltaddsubd  7645  ltaddsub2d  7646  leaddsub2d  7647  subled  7648  lesubd  7649  ltsub23d  7650  ltsub13d  7651  lesub1d  7652  lesub2d  7653  ltsub1d  7654  ltsub2d  7655  gt0add  7673  apcotr  7707  apadd1  7708  addext  7710  mulext1  7712  mulext  7714  gtapd  7735  leltapd  7737  subap0d  7740  mulap0  7744  divvalap  7762  divcanap2  7768  diveqap0  7770  divrecap  7776  divassap  7778  divmulassap  7783  divmulasscomap  7784  divdirap  7785  divcanap3  7786  div11ap  7788  rec11ap  7798  divmuldivap  7800  divdivdivap  7801  divmuleqap  7805  dmdcanap  7810  ddcanap  7814  divadddivap  7815  divsubdivap  7816  redivclap  7819  apmul1  7876  divclapd  7877  divcanap1d  7878  divcanap2d  7879  divrecapd  7880  divrecap2d  7881  divcanap3d  7882  divcanap4d  7883  diveqap0d  7884  diveqap1d  7885  diveqap1ad  7886  diveqap0ad  7887  divap0bd  7889  divnegapd  7890  divneg2apd  7891  div2negapd  7892  redivclapd  7920  ltmul12a  7938  lemul12b  7939  lt2mul2div  7957  ltdiv2  7965  ltdiv23  7970  avglt1  8269  avglt2  8270  lt2halvesd  8278  div4p1lem1div2  8284  zltp1le  8405  elz2  8419  zdivmul  8437  uztrn  8635  eluzsub  8648  uz3m2nn  8661  qaddcl  8720  cnref1o  8733  ltdiv2d  8797  lediv2d  8798  divlt1lt  8801  divle1le  8802  ledivge1le  8803  ltmulgt11d  8809  ltmulgt12d  8810  gt0divd  8811  ge0divd  8812  rpgecld  8813  ltmul1d  8815  ltmul2d  8816  lemul1d  8817  lemul2d  8818  ltdiv1d  8819  lediv1d  8820  ltmuldivd  8821  ltmuldiv2d  8822  lemuldivd  8823  lemuldiv2d  8824  ltdivmuld  8825  ltdivmul2d  8826  ledivmuld  8827  ledivmul2d  8828  ltdiv23d  8834  lediv23d  8835  addlelt  8839  xrltso  8871  xrlelttr  8876  xrlttrd  8879  xrlelttrd  8880  xrltletrd  8881  xrletrd  8882  xrre3  8889  ixxss1  8927  ixxss2  8928  ixxss12  8929  iooshf  8975  icoshftf1o  9013  ioodisj  9015  zltaddlt1le  9028  fznlem  9060  fzdifsuc  9098  fzrev  9101  fzrevral2  9123  elfz0fzfz0  9137  elfzmlbp  9143  fzctr  9144  elfzole1  9164  elfzolt2  9165  fzoss2  9181  fzospliti  9185  fzo1fzo0n0  9192  elfzo0z  9193  fzofzim  9197  fzoaddel  9201  eluzgtdifelfzo  9206  elfzodifsumelfzo  9210  ssfzo12bi  9234  elfzonelfzo  9239  fvinim0ffz  9250  qbtwnzlemex  9259  rebtwn2zlemstep  9261  rebtwn2z  9263  qbtwnxr  9266  flqge  9284  2tnp1ge0ge0  9303  intfracq  9322  flqdiv  9323  modqval  9326  modqcld  9330  modqmulnn  9344  zmodcl  9346  zmodfz  9348  modqid  9351  zmodid2  9354  modqabs  9359  modqcyc  9361  modqadd1  9363  modqaddabs  9364  modqaddmod  9365  mulp1mod1  9367  modqmuladd  9368  modqmuladdim  9369  modqmuladdnn0  9370  m1modnnsub1  9372  modqltm1p1mod  9378  modqmul1  9379  modqsubmod  9384  modqsubmodmod  9385  q2txmodxeq0  9386  modaddmodup  9389  modqmulmod  9391  modqaddmulmod  9393  modqdi  9394  modqsubdir  9395  addmodlteq  9400  frecuzrdgrrn  9410  frec2uzrdg  9411  frecuzrdgsuc  9417  frecfzen2  9420  iseqval  9440  iseqp1  9445  monoord  9455  expinnval  9479  expnegap0  9484  rpexpcl  9495  expnegzap  9510  expgt1  9514  mulexpzap  9516  exprecap  9517  expaddzaplem  9519  expaddzap  9520  expmul  9521  expmulzap  9522  expdivap  9527  ltexp2a  9528  leexp2a  9529  leexp2r  9530  leexp1a  9531  bernneq2  9594  bernneq3  9595  expnbnd  9596  expnlbnd  9597  expnlbnd2  9598  expaddd  9607  expmuld  9608  expclzapd  9610  expap0d  9611  expnegapd  9612  exprecapd  9613  expp1zapd  9614  expm1apd  9615  sqdivapd  9618  mulexpd  9620  expge0d  9623  expge1d  9624  sqoddm1div8  9625  reexpclzapd  9630  leexp2ad  9634  facwordi  9667  faclbnd3  9670  facavg  9673  bcval  9676  bccmpl  9681  bc0k  9683  ibcval5  9690  bcpasc  9693  shftfvalg  9706  mulreap  9751  cjreb  9753  cjap  9793  cnrecnv  9797  cjdivapd  9855  redivapd  9861  imdivapd  9862  resqrexlemdecn  9898  absexpzap  9966  abslt  9974  absle  9975  elicc4abs  9980  abs3lem  9997  fzomaxdiflem  9998  cau3lem  10000  amgm2  10004  abssubge0d  10062  abssuble0d  10063  absdifltd  10064  absdifled  10065  absdivapd  10081  abs3difd  10086  qdenre  10088  maxabslemlub  10093  rexanre  10106  rexico  10107  fimaxre2  10109  lemininf  10115  ltmininf  10116  climshftlemg  10141  climshft2  10145  addcn2  10149  mulcn2  10151  cn1lem  10152  climadd  10164  climmul  10165  climsub  10166  climsqz  10173  climsqz2  10174  climrecvg1n  10185  climcvg1nlem  10186  dvdsval3  10199  nndivdvds  10201  summodnegmod  10226  modmulconst  10227  dvds2subd  10231  dvdsmultr1d  10234  dvdsmultr2  10235  dvdsabseq  10247  dvdsfac  10260  dvdsmod  10262  oddge22np1  10281  ltoddhalfle  10293  halfleoddlt  10294  nn0ehalf  10303  nno  10306  nn0oddm1d2  10309  divalglemnn  10318  divalg  10324  divalgmod  10327  fldivndvdslt  10335  flodddiv4lt  10336  flodddiv4t2lthalf  10337  infssuzex  10345  dvdsbnd  10348  gcdneg  10373  gcdaddm  10375  modgcd  10382  bezoutlemnewy  10385  bezoutlemstep  10386  bezoutlembi  10394  dvdsgcdb  10402  gcdass  10404  mulgcd  10405  dvdsmulgcd  10414  rpmulgcd  10415  sqgcd  10418  nn0seqcvgd  10423  eucalglt  10439  gcddvdslcm  10455  lcmgcdlem  10459  lcmdvdsb  10466  lcmass  10467  ncoprmgcdne1b  10471  coprmdvds2  10475  mulgcddvds  10476  rpmulgcd2  10477  qredeu  10479  rpdvds  10481  divgcdcoprm0  10483  cncongr1  10485  cncongr2  10486  isprm2lem  10498  prmind2  10502  nprm  10505  dvdsnprmd  10507  exprmfct  10519  prmdvdsfz  10520  divgcdodd  10522  isprm6  10526  prmdvdsexp  10527  prmexpb  10530  prmfac1  10531  rpexp  10532  rpexp12i  10534  pw2dvdseulemle  10545  sqpweven  10553  2sqpwodd  10554