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  1333  eqeqan12d  2181  sylan9eq  2218  csbcomg  3067  sylan9ss  3154  ssconb  3254  ineqan12d  3324  dfopg  3755  breqan12d  3997  opexg  4205  copsex2g  4223  ordin  4362  onin  4363  unexg  4420  eusv1  4429  opelvvg  4652  opthprc  4654  opbrop  4682  relop  4753  dmpropg  5075  unixpm  5138  funssres  5229  funinsn  5236  funtp  5240  fnco  5295  resasplitss  5366  fodmrnu  5417  relrnfvex  5503  fconst2g  5699  oveqan12d  5860  ovi3  5974  ovg  5976  f1opw2  6043  off  6061  offres  6100  iunon  6248  nnsucsssuc  6456  nnaword1  6477  ertr  6512  erex  6521  brecop  6587  ecovdi  6608  ecovidi  6609  mapvalg  6620  pmvalg  6621  pmss12g  6637  mapsn  6652  en2sn  6775  xpf1o  6806  xpen  6807  phplem4  6817  ssfilem  6837  diffitest  6849  en1eqsn  6909  sbthlem7  6924  ordiso  6997  updjud  7043  fodju0  7107  finnum  7135  pr2nelem  7143  djucomen  7168  exmidontriimlem1  7173  ltsopi  7257  pitric  7258  pitri3or  7259  ltdcpi  7260  mulclpi  7265  addcompig  7266  mulcompig  7268  distrpig  7270  ltexpi  7274  ltapig  7275  ltmpig  7276  dfplpq2  7291  dfmpq2  7292  enqbreq2  7294  enqdc  7298  addcmpblnq  7304  addpipqqslem  7306  mulpipq2  7308  mulpipq  7309  mulpipqqs  7310  addclnq  7312  distrnqg  7324  ltdcnq  7334  ltrnqg  7357  enq0breq  7373  addclnq0  7388  nqnq0a  7391  nqnq0m  7392  nq0m0r  7393  distrnq0  7396  mulcomnq0  7397  genipv  7446  genplt2i  7447  genpelvl  7449  genpelvu  7450  addnqprlemrl  7494  addnqprlemru  7495  addnqprlemfl  7496  addnqprlemfu  7497  addnqpr  7498  mulnqprlemrl  7510  mulnqprlemru  7511  mulnqprlemfl  7512  mulnqprlemfu  7513  mulnqpr  7514  distrlem4prl  7521  distrlem4pru  7522  ltnqpr  7530  recexprlemloc  7568  archrecnq  7600  mulclsr  7691  1idsr  7705  00sr  7706  prsradd  7723  axmulass  7810  axdistr  7811  axcnre  7818  peano5nnnn  7829  mulid1  7892  axltadd  7964  lenlt  7970  cnegexlem3  8071  cnegex  8072  resubcl  8158  subeqrev  8270  muladd  8278  mulsub  8295  mulsub2  8296  ltaddsub2  8331  leaddsub2  8333  leltadd  8341  ltaddpos2  8347  posdif  8349  addge02  8367  mullt0  8374  recexre  8472  recextlem1  8544  recexap  8546  divmuldivap  8604  conjmulap  8621  div2subap  8729  prodgt02  8744  prodge02  8746  lemul2  8748  lemul2a  8750  ltmulgt12  8756  lemulge12  8758  ltmuldiv2  8766  ltdivmul2  8769  ledivmul2  8771  lemuldiv2  8773  negiso  8846  cju  8852  peano5nni  8856  nnaddcl  8873  nnmulcl  8874  nnsub  8892  addltmul  9089  avgle1  9093  avgle2  9094  nnrecl  9108  nn0nnaddcl  9141  zsubcl  9228  zleloe  9234  znnsub  9238  nzadd  9239  zmulcl  9240  zltp1le  9241  zleltp1  9242  nnleltp1  9246  nnltp1le  9247  nnaddm1cl  9248  nn0ltp1le  9249  nn0leltp1  9250  nn0ltlem1  9251  znn0sub  9252  nn0sub  9253  elz2  9258  zapne  9261  zdcle  9263  zdclt  9264  zltlen  9265  nn0lem1lt  9270  nnlem1lt  9271  nnltlem1  9272  zdiv  9275  zextle  9278  zextlt  9279  btwnnz  9281  prime  9286  nneo  9290  peano2uz2  9294  peano5uzti  9295  uzind  9298  fzind  9302  fnn0ind  9303  uzneg  9480  uz11  9484  eluzp1m1  9485  eluzp1p1  9487  uzin  9494  indstr  9527  uz2mulcl  9542  qre  9559  qaddcl  9569  qsubcl  9572  qltlen  9574  qlttri2  9575  irradd  9580  elpqb  9583  cnref1o  9584  rpaddcl  9609  rpmulcl  9610  rpdivcl  9611  rexadd  9784  rexsub  9785  xaddcom  9793  xnn0xadd0  9799  xnegdi  9800  elicc2  9870  iccshftr  9926  iccshftl  9928  iccdil  9930  icccntr  9932  fzval2  9943  elfz1eq  9966  peano2fzr  9968  fznlem  9972  fzsplit2  9981  fzaddel  9990  fzsubel  9991  fzrev2  10016  fzrev3  10018  uzsplit  10023  fzrevral  10036  fzrevral3  10038  fzshftral  10039  elfz2nn0  10043  fznn0sub2  10059  fz0fzdiffz0  10061  elfzmlbp  10063  difelfzle  10065  difelfznle  10066  1fv  10070  elfzouz2  10092  fzouzsplit  10110  elfzo0le  10116  fzonmapblen  10118  fzofzim  10119  fzoaddel2  10124  eluzgtdifelfzo  10128  elfzodifsumelfzo  10132  ubmelm1fzo  10157  fzofzp1b  10159  fzosplitprm1  10165  fzostep1  10168  subfzo0  10173  qbtwnxr  10189  flqbi2  10222  divfl0  10227  flqzadd  10229  flqmulnn0  10230  addmodidr  10304  modfzo0difsn  10326  frec2uzltd  10334  frec2uzrand  10336  frecfzen2  10358  seq3split  10410  seq3caopr2  10413  exp3vallem  10452  expcllem  10462  expcl2lemap  10463  1exp  10480  expge1  10488  expadd  10493  expmul  10496  expsubap  10499  leexp1a  10506  lt2sq  10524  le2sq  10525  sumsqeq0  10529  qsqeqor  10561  bernneq  10571  bernneq2  10572  sq11ap  10618  facdiv  10647  faclbnd  10650  faclbnd3  10652  faclbnd6  10653  facavg  10655  bcrpcl  10662  bccmpl  10663  fiubm  10737  seq3coll  10751  shftfvalg  10756  shftf  10768  crre  10795  crim  10796  mulreap  10802  readd  10807  resub  10808  remul2  10811  imadd  10815  imsub  10816  immul2  10818  ipcnval  10824  cjsub  10830  cjreim  10841  caucvgre  10919  rexanuz  10926  rexuz3  10928  resqrexlemover  10948  resqrexlemcvg  10957  resqrexlemglsq  10960  sqrtle  10974  sqrtlt  10975  sqrt11ap  10976  sqrt11  10977  absreimsq  11005  absreim  11006  absmul  11007  sqabs  11020  absdiflt  11030  absdifle  11031  abssuble0  11041  abs2difabs  11046  fzomaxdif  11051  caubnd2  11055  rpmaxcl  11161  zmaxcl  11162  minmax  11167  mincl  11168  min1inf  11169  min2inf  11170  minabs  11173  minclpr  11174  rpmincl  11175  2zinfmin  11180  xrmaxrecl  11192  xrminmax  11202  xrmincl  11203  xrmin1inf  11204  xrmin2inf  11205  xrminrecl  11210  xrminrpcl  11211  iooinsup  11214  climconst2  11228  climuni  11230  2clim  11238  climshft  11241  climshft2  11243  cjcn2  11253  climaddc1  11266  climmulc2  11268  climsubc1  11269  climsubc2  11270  climlec2  11278  summodclem2a  11318  zsumdc  11321  isumclim3  11360  mptfzshft  11379  fsumrev  11380  fisum0diag2  11384  telfsumo2  11404  fsumparts  11407  cvgcmpub  11413  binomlem  11420  binom1p  11422  binom1dif  11424  bcxmas  11426  isumshft  11427  expcnvap0  11439  expcnv  11441  geosergap  11443  geolim  11448  cvgratnnlemrate  11467  mertenslemi1  11472  mertenslem2  11473  mertensabs  11474  prodmodc  11515  zproddc  11516  fprodf1o  11525  fprodeq0  11554  efcj  11610  eftlub  11627  effsumlt  11629  efieq  11672  sinsub  11677  cossub  11678  subsin  11680  sinmul  11681  cosmul  11682  addcos  11683  subcos  11684  dvdssub2  11771  dvdsadd  11772  dvdsaddr  11773  dvdssub  11774  dvdssubr  11775  fzocongeq  11792  odd2np1  11806  opoe  11828  omoe  11829  opeo  11830  omeo  11831  divalgb  11858  ndvdsadd  11864  zsupcllemstep  11874  gcdabs  11917  dvdsgcd  11941  absmulgcd  11946  gcdmultiple  11949  gcdmultiplez  11950  rpmulgcd  11955  sqgcd  11958  dvdssqlem  11959  dvdssq  11960  nn0seqcvgd  11969  ialgrlemconst  11971  algrf  11973  algrp1  11974  algcvg  11976  algcvga  11979  lcmval  11991  lcmabs  12004  lcmgcd  12006  lcmdvds  12007  lcmgcdnn  12010  coprmgcdb  12016  coprmdvds  12020  coprmdvds2  12021  qredeq  12024  isprm3  12046  nprm  12051  divgcdodd  12071  prmdvdsexp  12076  sqrt2irr  12090  zgcdsq  12129  hashdvds  12149  phiprmpw  12150  crth  12152  phimullem  12153  modprm0  12182  coprimeprodsq  12185  coprimeprodsq2  12186  pythagtriplem2  12194  pythagtriplem19  12210  pcdvdsb  12247  pcneg  12252  pc2dvds  12257  pc11  12258  pcmpt  12269  pcfac  12276  infpnlem1  12285  prmunb  12288  1arithlem4  12292  1arith  12293  gzaddcl  12303  gzmulcl  12304  gzreim  12305  gzsubcl  12306  4sqlem1  12314  4sqlem4a  12317  4sqlem4  12318  setsvalg  12420  setsfun0  12426  restval  12557  innei  12763  cnovex  12796  txuni2  12856  txbasex  12857  txbas  12858  txtop  12860  txtopon  12862  txss12  12866  txbasval  12867  txcnp  12871  upxp  12872  txcnmpt  12873  uptx  12874  txcn  12875  txrest  12876  txdis  12877  cnmpt21  12891  hmeoco  12916  txhmeo  12919  isxmet2d  12948  blin2  13032  comet  13099  metcn  13114  txmetcn  13119  qtopbasss  13121  qtopbas  13122  remetdval  13139  bl2ioo  13142  blssioo  13145  divcnap  13155  cncfmet  13179  dvaddxxbr  13265  dvcjbr  13272  efle  13297  reapef  13299  sinperlem  13329  sincosq2sgn  13348  sincosq3sgn  13349  sincos6thpi  13363  ioocosf1o  13375  relogoprlem  13389  logleb  13396  cxple3  13441  cxpcom  13457  lgslem3  13503  lgsdir2  13534  lgsdir  13536  lgsdilem2  13537  lgsdi  13538  2sqlem2  13551  mul2sq  13552  2sqlem7  13557  bj-inex  13749  bj-bdfindis  13789  triap  13868  cvgcmp2nlemabs  13871  trilpolemisumle  13877  inffz  13908