Theorem syl2an 287

Description: A double syllogism inference. (Contributed by NM, 31-Jan-1997.)

Hypotheses

Ref	Expression
syl2an.1	|- ( ph -> ps )
syl2an.2	|- ( ta -> ch )
syl2an.3	|- ( ( ps /\ ch ) -> th )

Assertion

Ref	Expression
syl2an	|- ( ( ph /\ ta ) -> th )

Proof of Theorem syl2an

Step	Hyp	Ref	Expression
1		syl2an.2	. 2 |- ( ta -> ch )
2		syl2an.1	. . 3 |- ( ph -> ps )
3		syl2an.3	. . 3 |- ( ( ps /\ ch ) -> th )
4	2, 3	sylan 281	. 2 |- ( ( ph /\ ch ) -> th )
5	1, 4	sylan2 284	1 |- ( ( ph /\ ta ) -> th )

Syntax hints:   -> wi 4   /\ wa 103

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 is referenced by:  syl2anr  288  anim12i  336  syl2an2  584  syl2an2r  585  mp3an3an  1322  eqeqan12d  2156  sylan9eq  2193  csbcomg  3030  sylan9ss  3115  ssconb  3214  ineqan12d  3284  dfopg  3711  breqan12d  3953  opexg  4158  copsex2g  4176  ordin  4315  onin  4316  unexg  4372  eusv1  4381  opelvvg  4596  opthprc  4598  opbrop  4626  relop  4697  dmpropg  5019  unixpm  5082  funssres  5173  funinsn  5180  funtp  5184  fnco  5239  resasplitss  5310  fodmrnu  5361  relrnfvex  5447  fconst2g  5643  oveqan12d  5801  ovi3  5915  ovg  5917  f1opw2  5984  off  6002  offres  6041  iunon  6189  nnsucsssuc  6396  nnaword1  6417  ertr  6452  erex  6461  brecop  6527  ecovdi  6548  ecovidi  6549  mapvalg  6560  pmvalg  6561  pmss12g  6577  mapsn  6592  en2sn  6715  xpf1o  6746  xpen  6747  phplem4  6757  ssfilem  6777  diffitest  6789  en1eqsn  6844  sbthlem7  6859  ordiso  6929  updjud  6975  fodju0  7027  finnum  7056  pr2nelem  7064  djucomen  7089  ltsopi  7152  pitric  7153  pitri3or  7154  ltdcpi  7155  mulclpi  7160  addcompig  7161  mulcompig  7163  distrpig  7165  ltexpi  7169  ltapig  7170  ltmpig  7171  dfplpq2  7186  dfmpq2  7187  enqbreq2  7189  enqdc  7193  addcmpblnq  7199  addpipqqslem  7201  mulpipq2  7203  mulpipq  7204  mulpipqqs  7205  addclnq  7207  distrnqg  7219  ltdcnq  7229  ltrnqg  7252  enq0breq  7268  addclnq0  7283  nqnq0a  7286  nqnq0m  7287  nq0m0r  7288  distrnq0  7291  mulcomnq0  7292  genipv  7341  genplt2i  7342  genpelvl  7344  genpelvu  7345  addnqprlemrl  7389  addnqprlemru  7390  addnqprlemfl  7391  addnqprlemfu  7392  addnqpr  7393  mulnqprlemrl  7405  mulnqprlemru  7406  mulnqprlemfl  7407  mulnqprlemfu  7408  mulnqpr  7409  distrlem4prl  7416  distrlem4pru  7417  ltnqpr  7425  recexprlemloc  7463  archrecnq  7495  mulclsr  7586  1idsr  7600  00sr  7601  prsradd  7618  axmulass  7705  axdistr  7706  axcnre  7713  peano5nnnn  7724  mulid1  7787  axltadd  7858  lenlt  7864  cnegexlem3  7963  cnegex  7964  resubcl  8050  subeqrev  8162  muladd  8170  mulsub  8187  mulsub2  8188  ltaddsub2  8223  leaddsub2  8225  leltadd  8233  ltaddpos2  8239  posdif  8241  addge02  8259  mullt0  8266  recexre  8364  recextlem1  8436  recexap  8438  divmuldivap  8496  conjmulap  8513  div2subap  8620  prodgt02  8635  prodge02  8637  lemul2  8639  lemul2a  8641  ltmulgt12  8647  lemulge12  8649  ltmuldiv2  8657  ltdivmul2  8660  ledivmul2  8662  lemuldiv2  8664  negiso  8737  cju  8743  peano5nni  8747  nnaddcl  8764  nnmulcl  8765  nnsub  8783  addltmul  8980  avgle1  8984  avgle2  8985  nnrecl  8999  nn0nnaddcl  9032  zsubcl  9119  zleloe  9125  znnsub  9129  nzadd  9130  zmulcl  9131  zltp1le  9132  zleltp1  9133  nnleltp1  9137  nnltp1le  9138  nnaddm1cl  9139  nn0ltp1le  9140  nn0leltp1  9141  nn0ltlem1  9142  znn0sub  9143  nn0sub  9144  elz2  9146  zapne  9149  zdcle  9151  zdclt  9152  zltlen  9153  nn0lem1lt  9158  nnlem1lt  9159  nnltlem1  9160  zdiv  9163  zextle  9166  zextlt  9167  btwnnz  9169  prime  9174  nneo  9178  peano2uz2  9182  peano5uzti  9183  uzind  9186  fzind  9190  fnn0ind  9191  uzneg  9368  uz11  9372  eluzp1m1  9373  eluzp1p1  9375  uzin  9382  indstr  9415  uz2mulcl  9429  qre  9444  qaddcl  9454  qsubcl  9457  qltlen  9459  qlttri2  9460  irradd  9465  elpqb  9468  cnref1o  9469  rpaddcl  9494  rpmulcl  9495  rpdivcl  9496  rexadd  9665  rexsub  9666  xaddcom  9674  xnn0xadd0  9680  xnegdi  9681  elicc2  9751  iccshftr  9807  iccshftl  9809  iccdil  9811  icccntr  9813  fzval2  9824  elfz1eq  9846  peano2fzr  9848  fznlem  9852  fzsplit2  9861  fzaddel  9870  fzsubel  9871  fzrev2  9896  fzrev3  9898  uzsplit  9903  fzrevral  9916  fzrevral3  9918  fzshftral  9919  elfz2nn0  9923  fznn0sub2  9936  fz0fzdiffz0  9938  elfzmlbp  9940  difelfzle  9942  difelfznle  9943  1fv  9947  elfzouz2  9969  fzouzsplit  9987  elfzo0le  9993  fzonmapblen  9995  fzofzim  9996  fzoaddel2  10001  eluzgtdifelfzo  10005  elfzodifsumelfzo  10009  ubmelm1fzo  10034  fzofzp1b  10036  fzosplitprm1  10042  fzostep1  10045  subfzo0  10050  qbtwnxr  10066  flqbi2  10095  divfl0  10100  flqzadd  10102  flqmulnn0  10103  addmodidr  10177  modfzo0difsn  10199  frec2uzltd  10207  frec2uzrand  10209  frecfzen2  10231  seq3split  10283  seq3caopr2  10286  exp3vallem  10325  expcllem  10335  expcl2lemap  10336  1exp  10353  expge1  10361  expadd  10366  expmul  10369  expsubap  10372  leexp1a  10379  lt2sq  10397  le2sq  10398  sumsqeq0  10402  bernneq  10443  bernneq2  10444  sq11ap  10489  facdiv  10516  faclbnd  10519  faclbnd3  10521  faclbnd6  10522  facavg  10524  bcrpcl  10531  bccmpl  10532  seq3coll  10617  shftfvalg  10622  shftf  10634  crre  10661  crim  10662  mulreap  10668  readd  10673  resub  10674  remul2  10677  imadd  10681  imsub  10682  immul2  10684  ipcnval  10690  cjsub  10696  cjreim  10707  caucvgre  10785  rexanuz  10792  rexuz3  10794  resqrexlemover  10814  resqrexlemcvg  10823  resqrexlemglsq  10826  sqrtle  10840  sqrtlt  10841  sqrt11ap  10842  sqrt11  10843  absreimsq  10871  absreim  10872  absmul  10873  sqabs  10886  absdiflt  10896  absdifle  10897  abssuble0  10907  abs2difabs  10912  fzomaxdif  10917  caubnd2  10921  rpmaxcl  11027  zmaxcl  11028  minmax  11033  mincl  11034  min1inf  11035  min2inf  11036  minabs  11039  minclpr  11040  rpmincl  11041  xrmaxrecl  11056  xrminmax  11066  xrmincl  11067  xrmin1inf  11068  xrmin2inf  11069  xrminrecl  11074  xrminrpcl  11075  iooinsup  11078  climconst2  11092  climuni  11094  2clim  11102  climshft  11105  climshft2  11107  cjcn2  11117  climaddc1  11130  climmulc2  11132  climsubc1  11133  climsubc2  11134  climlec2  11142  summodclem2a  11182  zsumdc  11185  isumclim3  11224  mptfzshft  11243  fsumrev  11244  fisum0diag2  11248  telfsumo2  11268  fsumparts  11271  cvgcmpub  11277  binomlem  11284  binom1p  11286  binom1dif  11288  bcxmas  11290  isumshft  11291  expcnvap0  11303  expcnv  11305  geosergap  11307  geolim  11312  cvgratnnlemrate  11331  mertenslemi1  11336  mertenslem2  11337  mertensabs  11338  prodmodc  11379  zproddc  11380  efcj  11416  eftlub  11433  effsumlt  11435  efieq  11478  sinsub  11483  cossub  11484  subsin  11486  sinmul  11487  cosmul  11488  addcos  11489  subcos  11490  dvdssub2  11571  dvdsadd  11572  dvdsaddr  11573  dvdssub  11574  dvdssubr  11575  fzocongeq  11592  odd2np1  11606  opoe  11628  omoe  11629  opeo  11630  omeo  11631  divalgb  11658  ndvdsadd  11664  zsupcllemstep  11674  gcdabs  11712  dvdsgcd  11736  absmulgcd  11741  gcdmultiple  11744  gcdmultiplez  11745  rpmulgcd  11750  sqgcd  11753  dvdssqlem  11754  dvdssq  11755  nn0seqcvgd  11758  ialgrlemconst  11760  algrf  11762  algrp1  11763  algcvg  11765  algcvga  11768  lcmval  11780  lcmabs  11793  lcmgcd  11795  lcmdvds  11796  lcmgcdnn  11799  coprmgcdb  11805  coprmdvds  11809  coprmdvds2  11810  qredeq  11813  isprm3  11835  nprm  11840  divgcdodd  11857  prmdvdsexp  11862  sqrt2irr  11876  zgcdsq  11915  hashdvds  11933  phiprmpw  11934  crth  11936  phimullem  11937  setsvalg  12028  setsfun0  12034  restval  12165  innei  12371  cnovex  12404  txuni2  12464  txbasex  12465  txbas  12466  txtop  12468  txtopon  12470  txss12  12474  txbasval  12475  txcnp  12479  upxp  12480  txcnmpt  12481  uptx  12482  txcn  12483  txrest  12484  txdis  12485  cnmpt21  12499  hmeoco  12524  txhmeo  12527  isxmet2d  12556  blin2  12640  comet  12707  metcn  12722  txmetcn  12727  qtopbasss  12729  qtopbas  12730  remetdval  12747  bl2ioo  12750  blssioo  12753  divcnap  12763  cncfmet  12787  dvaddxxbr  12873  dvcjbr  12880  efle  12905  reapef  12907  sinperlem  12937  sincosq2sgn  12956  sincosq3sgn  12957  sincos6thpi  12971  ioocosf1o  12983  relogoprlem  12997  logleb  13004  cxple3  13049  cxpcom  13065  bj-inex  13276  bj-bdfindis  13316  triap  13399  cvgcmp2nlemabs  13402  trilpolemisumle  13406  inffz  13429