Theorem syl2an 289

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 283	. 2 |- ( ( ph /\ ch ) -> th )
5	1, 4	sylan2 286	1 |- ( ( ph /\ ta ) -> th )

Syntax hints:   -> wi 4   /\ wa 104

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

This theorem is referenced by:  syl2anr  290  anim12i  338  syl2an2  594  syl2an2r  595  orandc  941  mp3an3an  1354  eqeqan12d  2212  sylan9eq  2249  csbcomg  3107  sylan9ss  3196  ssconb  3296  ineqan12d  3366  dfopg  3806  breqan12d  4049  opexg  4261  copsex2g  4279  ordin  4420  onin  4421  unexg  4478  eusv1  4487  opelvvg  4712  opthprc  4714  opbrop  4742  relop  4816  dmpropg  5142  unixpm  5205  funssres  5300  funinsn  5307  funtp  5311  fnco  5366  resasplitss  5437  fodmrnu  5488  relrnfvex  5576  fconst2g  5777  oveqan12d  5941  ovi3  6060  ovg  6062  f1opw2  6129  off  6148  offres  6192  iunon  6342  nnsucsssuc  6550  nnaword1  6571  ertr  6607  erex  6616  brecop  6684  ecovdi  6705  ecovidi  6706  mapvalg  6717  pmvalg  6718  pmss12g  6734  mapsn  6749  en2sn  6872  xpf1o  6905  xpen  6906  phplem4  6916  ssfilem  6936  diffitest  6948  en1eqsn  7014  sbthlem7  7029  ordiso  7102  updjud  7148  fodju0  7213  finnum  7250  pr2nelem  7258  djucomen  7283  exmidontriimlem1  7288  2onetap  7322  ltsopi  7387  pitric  7388  pitri3or  7389  ltdcpi  7390  mulclpi  7395  addcompig  7396  mulcompig  7398  distrpig  7400  ltexpi  7404  ltapig  7405  ltmpig  7406  dfplpq2  7421  dfmpq2  7422  enqbreq2  7424  enqdc  7428  addcmpblnq  7434  addpipqqslem  7436  mulpipq2  7438  mulpipq  7439  mulpipqqs  7440  addclnq  7442  distrnqg  7454  ltdcnq  7464  ltrnqg  7487  enq0breq  7503  addclnq0  7518  nqnq0a  7521  nqnq0m  7522  nq0m0r  7523  distrnq0  7526  mulcomnq0  7527  genipv  7576  genplt2i  7577  genpelvl  7579  genpelvu  7580  addnqprlemrl  7624  addnqprlemru  7625  addnqprlemfl  7626  addnqprlemfu  7627  addnqpr  7628  mulnqprlemrl  7640  mulnqprlemru  7641  mulnqprlemfl  7642  mulnqprlemfu  7643  mulnqpr  7644  distrlem4prl  7651  distrlem4pru  7652  ltnqpr  7660  recexprlemloc  7698  archrecnq  7730  mulclsr  7821  1idsr  7835  00sr  7836  prsradd  7853  axmulass  7940  axdistr  7941  axcnre  7948  peano5nnnn  7959  mulrid  8023  axltadd  8096  lenlt  8102  cnegexlem3  8203  cnegex  8204  resubcl  8290  subeqrev  8402  muladd  8410  mulsub  8427  mulsub2  8428  ltaddsub2  8464  leaddsub2  8466  leltadd  8474  ltaddpos2  8480  posdif  8482  addge02  8500  mullt0  8507  recexre  8605  recextlem1  8678  recexap  8680  divmuldivap  8739  conjmulap  8756  div2subap  8864  prodgt02  8880  prodge02  8882  lemul2  8884  lemul2a  8886  ltmulgt12  8892  lemulge12  8894  ltmuldiv2  8902  ltdivmul2  8905  ledivmul2  8907  lemuldiv2  8909  negiso  8982  cju  8988  peano5nni  8993  nnaddcl  9010  nnmulcl  9011  nnsub  9029  addltmul  9228  avgle1  9232  avgle2  9233  nnrecl  9247  nn0nnaddcl  9280  zsubcl  9367  zleloe  9373  znnsub  9377  nzadd  9378  zmulcl  9379  zltp1le  9380  zleltp1  9381  nnleltp1  9385  nnltp1le  9386  nnaddm1cl  9387  nn0ltp1le  9388  nn0leltp1  9389  nn0ltlem1  9390  znn0sub  9391  nn0sub  9392  elz2  9397  zapne  9400  zdcle  9402  zdclt  9403  zltlen  9404  nn0lem1lt  9409  nnlem1lt  9410  nnltlem1  9411  zdiv  9414  zextle  9417  zextlt  9418  btwnnz  9420  prime  9425  nneo  9429  peano2uz2  9433  peano5uzti  9434  uzind  9437  fzind  9441  fnn0ind  9442  uzneg  9620  uz11  9624  eluzp1m1  9625  eluzp1p1  9627  uzin  9634  indstr  9667  uz2mulcl  9682  qre  9699  qaddcl  9709  qsubcl  9712  qltlen  9714  qlttri2  9715  irradd  9720  elpqb  9724  cnref1o  9725  rpaddcl  9752  rpmulcl  9753  rpdivcl  9754  rexadd  9927  rexsub  9928  xaddcom  9936  xnn0xadd0  9942  xnegdi  9943  elicc2  10013  iccshftr  10069  iccshftl  10071  iccdil  10073  icccntr  10075  fzval2  10086  elfz1eq  10110  peano2fzr  10112  fznlem  10116  fzsplit2  10125  fzaddel  10134  fzsubel  10135  fzrev2  10160  fzrev3  10162  uzsplit  10167  fzrevral  10180  fzrevral3  10182  fzshftral  10183  elfz2nn0  10187  fznn0sub2  10203  fz0fzdiffz0  10205  elfzmlbp  10207  difelfzle  10209  difelfznle  10210  1fv  10214  elfzouz2  10237  fzouzsplit  10255  elfzo0le  10261  fzonmapblen  10263  fzofzim  10264  fzoaddel2  10269  eluzgtdifelfzo  10273  elfzodifsumelfzo  10277  ubmelm1fzo  10302  fzofzp1b  10304  fzosplitprm1  10310  fzostep1  10313  subfzo0  10318  zsupcllemstep  10319  qdclt  10335  qbtwnxr  10347  flqbi2  10381  divfl0  10386  flqzadd  10388  flqmulnn0  10389  addmodidr  10465  modfzo0difsn  10487  frec2uzltd  10495  frec2uzrand  10497  frecfzen2  10519  seqshft2g  10574  seq3split  10580  seqsplitg  10581  seq3caopr2  10585  seqcaopr2g  10586  seqf1oglem2  10612  exp3vallem  10632  expcllem  10642  expcl2lemap  10643  1exp  10660  expge1  10668  expadd  10673  expmul  10676  expsubap  10679  leexp1a  10686  lt2sq  10705  le2sq  10706  sumsqeq0  10710  qsqeqor  10742  bernneq  10752  bernneq2  10753  sq11ap  10799  facdiv  10830  faclbnd  10833  faclbnd3  10835  faclbnd6  10836  facavg  10838  bcrpcl  10845  bccmpl  10846  fiubm  10920  seq3coll  10934  eqwrd  10975  shftfvalg  10983  shftf  10995  crre  11022  crim  11023  mulreap  11029  readd  11034  resub  11035  remul2  11038  imadd  11042  imsub  11043  immul2  11045  ipcnval  11051  cjsub  11057  cjreim  11068  caucvgre  11146  rexanuz  11153  rexuz3  11155  resqrexlemover  11175  resqrexlemcvg  11184  resqrexlemglsq  11187  sqrtle  11201  sqrtlt  11202  sqrt11ap  11203  sqrt11  11204  absreimsq  11232  absreim  11233  absmul  11234  sqabs  11247  absdiflt  11257  absdifle  11258  abssuble0  11268  abs2difabs  11273  fzomaxdif  11278  caubnd2  11282  rpmaxcl  11388  zmaxcl  11389  nn0maxcl  11390  minmax  11395  mincl  11396  min1inf  11397  min2inf  11398  minabs  11401  minclpr  11402  rpmincl  11403  2zinfmin  11408  xrmaxrecl  11420  xrminmax  11430  xrmincl  11431  xrmin1inf  11432  xrmin2inf  11433  xrminrecl  11438  xrminrpcl  11439  iooinsup  11442  climconst2  11456  climuni  11458  2clim  11466  climshft  11469  climshft2  11471  cjcn2  11481  climaddc1  11494  climmulc2  11496  climsubc1  11497  climsubc2  11498  climlec2  11506  summodclem2a  11546  zsumdc  11549  isumclim3  11588  mptfzshft  11607  fsumrev  11608  fisum0diag2  11612  telfsumo2  11632  fsumparts  11635  cvgcmpub  11641  binomlem  11648  binom1p  11650  binom1dif  11652  bcxmas  11654  isumshft  11655  expcnvap0  11667  expcnv  11669  geosergap  11671  geolim  11676  cvgratnnlemrate  11695  mertenslemi1  11700  mertenslem2  11701  mertensabs  11702  prodmodc  11743  zproddc  11744  fprodf1o  11753  fprodeq0  11782  efcj  11838  eftlub  11855  effsumlt  11857  efieq  11900  sinsub  11905  cossub  11906  subsin  11908  sinmul  11909  cosmul  11910  addcos  11911  subcos  11912  dvdssub2  12000  dvdsadd  12001  dvdsaddr  12002  dvdssub  12003  dvdssubr  12004  fzocongeq  12023  odd2np1  12038  opoe  12060  omoe  12061  opeo  12062  omeo  12063  divalgb  12090  ndvdsadd  12096  gcdmndc  12122  gcdabs  12155  dvdsgcd  12179  absmulgcd  12184  gcdmultiple  12187  gcdmultiplez  12188  rpmulgcd  12193  sqgcd  12196  dvdssqlem  12197  dvdssq  12198  nninfctlemfo  12207  nn0seqcvgd  12209  ialgrlemconst  12211  algrf  12213  algrp1  12214  algcvg  12216  algcvga  12219  lcmval  12231  lcmabs  12244  lcmgcd  12246  lcmdvds  12247  lcmgcdnn  12250  coprmgcdb  12256  coprmdvds  12260  coprmdvds2  12261  qredeq  12264  isprm3  12286  nprm  12291  divgcdodd  12311  prmdvdsexp  12316  sqrt2irr  12330  zgcdsq  12369  hashdvds  12389  phiprmpw  12390  crth  12392  phimullem  12393  modprm0  12423  coprimeprodsq  12426  coprimeprodsq2  12427  pythagtriplem2  12435  pythagtriplem19  12451  pcdvdsb  12489  pcneg  12494  pc2dvds  12499  pc11  12500  pcmpt  12512  pcfac  12519  infpnlem1  12528  prmunb  12531  1arithlem4  12535  1arith  12536  gzaddcl  12546  gzmulcl  12547  gzreim  12548  gzsubcl  12549  4sqlem1  12557  4sqlem4a  12560  4sqlem4  12561  4sqlem12  12571  setsvalg  12708  setsfun0  12714  restval  12916  xpsval  12995  mndinvmod  13086  resmhm  13119  resmhm2  13120  mhmco  13122  dfgrp3m  13231  mhmmnd  13246  mulgnngsum  13257  mulgnn0z  13279  mulgnndir  13281  ghmex  13385  0ghm  13388  resghm  13390  resghm2  13391  ghmco  13394  ghmeql  13397  kerf1ghm  13404  ablsubsub23  13455  dfrhm2  13710  isrhm  13714  rhmfn  13728  rhmval  13729  rhmco  13730  resrhm  13804  rhmeql  13806  rhmima  13807  lmodfopne  13882  lspf  13945  znidom  14213  znrrg  14216  innei  14399  cnovex  14432  txuni2  14492  txbasex  14493  txbas  14494  txtop  14496  txtopon  14498  txss12  14502  txbasval  14503  txcnp  14507  upxp  14508  txcnmpt  14509  uptx  14510  txcn  14511  txrest  14512  txdis  14513  cnmpt21  14527  hmeoco  14552  txhmeo  14555  isxmet2d  14584  blin2  14668  comet  14735  metcn  14750  txmetcn  14755  qtopbasss  14757  qtopbas  14758  remetdval  14783  bl2ioo  14786  blssioo  14789  divcnap  14801  cncfmet  14828  dvaddxxbr  14937  dvcjbr  14944  plyf  14973  ply1termlem  14978  plymullem1  14984  plyaddlem  14985  plymullem  14986  plycolemc  14994  plyreres  15000  dvply1  15001  efle  15012  reapef  15014  sinperlem  15044  sincosq2sgn  15063  sincosq3sgn  15064  sincos6thpi  15078  ioocosf1o  15090  relogoprlem  15104  logleb  15111  cxple3  15157  cxpcom  15174  dvdsppwf1o  15225  fsumdvdsmul  15227  1sgmprm  15230  mersenne  15233  lgslem3  15243  lgsdir2  15274  lgsdir  15276  lgsdilem2  15277  lgsdi  15278  gausslemma2dlem1a  15299  gausslemma2dlem3  15304  gausslemma2dlem6  15308  lgseisenlem3  15313  lgseisenlem4  15314  lgsquadlem1  15318  lgsquadlem2  15319  lgsquad2  15324  lgsquad3  15325  2lgslem1a1  15327  2lgslem1a  15329  2lgslem1c  15331  2sqlem2  15356  mul2sq  15357  2sqlem7  15362  bj-inex  15553  bj-bdfindis  15593  triap  15673  cvgcmp2nlemabs  15676  trilpolemisumle  15682  inffz  15716