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  598  syl2an2r  599  orandc  948  mp3an3an  1380  eqeqan12d  2250  sylan9eq  2287  csbcomg  3164  sylan9ss  3255  ssconb  3356  ineqan12d  3428  dfopg  3886  breqan12d  4130  opexg  4349  copsex2g  4367  ordin  4511  onin  4512  unexg  4569  eusv1  4578  opelvvg  4804  opthprc  4806  opbrop  4834  relop  4910  dmpropg  5240  unixpm  5303  funssres  5400  funinsn  5410  funtp  5414  fnco  5471  resasplitss  5549  fodmrnu  5603  relrnfvex  5693  funopdmsn  5869  fconst2g  5904  oveqan12d  6077  ovi3  6199  ovg  6201  f1opw2  6269  off  6288  offres  6341  suppfnss  6470  iunon  6528  nnsucsssuc  6738  nnaword1  6759  ertr  6795  erex  6804  brecop  6872  ecovdi  6893  ecovidi  6894  mapvalg  6905  pmvalg  6906  pmss12g  6922  mapsn  6938  en2sn  7068  xpf1o  7110  xpen  7111  phplem4  7122  ssfilem  7143  ssfilemd  7145  diffitest  7157  en1eqsn  7231  sbthlem7  7246  fsuppxpfi  7262  ordiso  7340  updjud  7386  fodju0  7451  finnum  7492  pr2nelem  7501  djucomen  7536  exmidontriimlem1  7541  2onetap  7585  ltsopi  7651  pitric  7652  pitri3or  7653  ltdcpi  7654  mulclpi  7659  addcompig  7660  mulcompig  7662  distrpig  7664  ltexpi  7668  ltapig  7669  ltmpig  7670  dfplpq2  7685  dfmpq2  7686  enqbreq2  7688  enqdc  7692  addcmpblnq  7698  addpipqqslem  7700  mulpipq2  7702  mulpipq  7703  mulpipqqs  7704  addclnq  7706  distrnqg  7718  ltdcnq  7728  ltrnqg  7751  enq0breq  7767  addclnq0  7782  nqnq0a  7785  nqnq0m  7786  nq0m0r  7787  distrnq0  7790  mulcomnq0  7791  genipv  7840  genplt2i  7841  genpelvl  7843  genpelvu  7844  addnqprlemrl  7888  addnqprlemru  7889  addnqprlemfl  7890  addnqprlemfu  7891  addnqpr  7892  mulnqprlemrl  7904  mulnqprlemru  7905  mulnqprlemfl  7906  mulnqprlemfu  7907  mulnqpr  7908  distrlem4prl  7915  distrlem4pru  7916  ltnqpr  7924  recexprlemloc  7962  archrecnq  7994  mulclsr  8085  1idsr  8099  00sr  8100  prsradd  8117  axmulass  8204  axdistr  8205  axcnre  8212  peano5nnnn  8223  mulrid  8287  axltadd  8359  lenlt  8365  cnegexlem3  8466  cnegex  8467  resubcl  8553  subeqrev  8665  muladd  8674  mulsub  8691  mulsub2  8692  ltaddsub2  8728  leaddsub2  8730  leltadd  8738  ltaddpos2  8744  posdif  8746  addge02  8764  mullt0  8771  recexre  8869  recextlem1  8942  recexap  8944  divmuldivap  9003  conjmulap  9020  div2subap  9128  prodgt02  9144  prodge02  9146  lemul2  9148  lemul2a  9150  ltmulgt12  9156  lemulge12  9158  ltmuldiv2  9166  ltdivmul2  9169  ledivmul2  9171  lemuldiv2  9173  negiso  9246  cju  9252  peano5nni  9257  nnaddcl  9274  nnmulcl  9275  nnsub  9293  addltmul  9492  avgle1  9496  avgle2  9497  nnrecl  9511  nn0nnaddcl  9544  zsubcl  9635  zleloe  9641  znnsub  9646  nzadd  9647  zmulcl  9648  zltp1le  9649  zleltp1  9650  nnleltp1  9654  nnltp1le  9655  nnaddm1cl  9656  nn0ltp1le  9657  nn0leltp1  9658  nn0ltlem1  9659  znn0sub  9660  nn0sub  9661  elz2  9666  zapne  9669  zdcle  9671  zdclt  9672  zltlen  9674  nn0lem1lt  9679  nnlem1lt  9680  nnltlem1  9681  zdiv  9684  zextle  9687  zextlt  9688  btwnnz  9690  prime  9695  nneo  9699  peano2uz2  9703  peano5uzti  9704  uzind  9707  fzind  9711  fnn0ind  9712  uzneg  9891  uz11  9895  eluzp1m1  9896  eluzp1p1  9898  uzin  9905  indstr  9943  uz2mulcl  9958  qre  9975  qaddcl  9985  qsubcl  9988  qltlen  9990  qlttri2  9991  irradd  9996  elpqb  10000  cnref1o  10001  rpaddcl  10028  rpmulcl  10029  rpdivcl  10030  rexadd  10204  rexsub  10205  xaddcom  10213  xnn0xadd0  10219  xnegdi  10220  elicc2  10290  iccshftr  10346  iccshftl  10348  iccdil  10350  icccntr  10352  fzval2  10364  elfz1eq  10389  peano2fzr  10391  fznlem  10395  fzsplit2  10404  fzsplit3  10407  fzaddel  10414  fzsubel  10415  fzrev2  10441  fzrev3  10443  uzsplit  10448  fzrevral  10461  fzrevral3  10463  fzshftral  10464  elfz2nn0  10468  fznn0sub2  10484  fz0fzdiffz0  10486  elfzmlbp  10488  difelfzle  10490  difelfznle  10491  1fv  10495  elfzouz2  10518  fzo0n  10524  fzouzsplit  10537  fzoun  10539  elfzo0le  10546  fzonmapblen  10548  fzofzim  10549  fzoaddel2  10557  eluzgtdifelfzo  10564  elfzodifsumelfzo  10568  ubmelm1fzo  10593  fzofzp1b  10595  fzosplitprm1  10602  fzostep1  10605  subfzo0  10610  zsupcllemstep  10611  qdclt  10629  qbtwnxr  10641  flqbi2  10675  divfl0  10680  flqzadd  10682  flqmulnn0  10683  addmodidr  10759  modfzo0difsn  10781  frec2uzltd  10789  frec2uzrand  10791  frecfzen2  10813  seqshft2g  10868  seq3split  10874  seqsplitg  10875  seq3caopr2  10879  seqcaopr2g  10880  seqf1oglem2  10906  exp3vallem  10926  expcllem  10936  expcl2lemap  10937  1exp  10954  expge1  10962  expadd  10967  expmul  10970  expsubap  10973  leexp1a  10980  lt2sq  10999  le2sq  11000  sumsqeq0  11004  qsqeqor  11036  bernneq  11047  bernneq2  11048  sq11ap  11094  facdiv  11125  faclbnd  11128  faclbnd3  11130  faclbnd6  11131  facavg  11133  bcrpcl  11140  bccmpl  11141  bcm1n  11156  fiubm  11220  seq3coll  11239  eqwrd  11290  ccatcl  11306  ccatclab  11307  ccatlen  11308  ccat0  11309  ccatval1  11310  ccatval2  11311  elfzelfzccat  11313  ccatvalfn  11314  ccatsymb  11315  ccatval21sw  11318  ccatrn  11322  lswccatn0lsw  11324  ccatalpha  11326  ccatrcl1  11327  swrdfv2  11380  swrdsbslen  11383  swrdspsleq  11384  swrdccat2  11388  pfxclz  11396  ccatpfx  11418  pfxccat1  11419  swrdswrdlem  11421  pfxswrd  11423  pfxccatin12lem4  11443  pfxccatin12lem1  11445  pfxccatin12lem2  11448  pfxccatin12lem3  11449  pfxccat3  11451  swrdccat  11452  pfxccatpfx2  11454  pfxccat3a  11455  swrdccat3blem  11456  swrdccat3b  11457  s2dmg  11507  shftfvalg  11528  shftf  11540  crre  11567  crim  11568  mulreap  11574  readd  11579  resub  11580  remul2  11583  imadd  11587  imsub  11588  immul2  11590  ipcnval  11596  cjsub  11602  cjreim  11613  caucvgre  11691  rexanuz  11698  rexuz3  11700  resqrexlemover  11720  resqrexlemcvg  11729  resqrexlemglsq  11732  sqrtle  11746  sqrtlt  11747  sqrt11ap  11748  sqrt11  11749  absreimsq  11777  absreim  11778  absmul  11779  sqabs  11792  absdiflt  11802  absdifle  11803  abssuble0  11813  abs2difabs  11818  fzomaxdif  11823  caubnd2  11827  rpmaxcl  11933  zmaxcl  11934  nn0maxcl  11935  minmax  11940  mincl  11941  min1inf  11942  min2inf  11943  minabs  11946  minclpr  11947  rpmincl  11948  2zinfmin  11953  xrmaxrecl  11965  xrminmax  11975  xrmincl  11976  xrmin1inf  11977  xrmin2inf  11978  xrminrecl  11983  xrminrpcl  11984  iooinsup  11987  climconst2  12001  climuni  12003  2clim  12011  climshft  12014  climshft2  12016  cjcn2  12026  climaddc1  12039  climmulc2  12041  climsubc1  12042  climsubc2  12043  climlec2  12051  summodclem2a  12092  zsumdc  12095  isumclim3  12134  mptfzshft  12153  fsumrev  12154  fisum0diag2  12158  telfsumo2  12178  fsumparts  12181  cvgcmpub  12187  binomlem  12194  binom1p  12196  binom1dif  12198  bcxmas  12200  isumshft  12201  expcnvap0  12213  expcnv  12215  geosergap  12217  geolim  12222  cvgratnnlemrate  12241  mertenslemi1  12246  mertenslem2  12247  mertensabs  12248  prodmodc  12289  zproddc  12290  fprodf1o  12299  fprodeq0  12328  efcj  12384  eftlub  12401  effsumlt  12403  efieq  12446  sinsub  12451  cossub  12452  subsin  12454  sinmul  12455  cosmul  12456  addcos  12457  subcos  12458  dvdssub2  12546  dvdsadd  12547  dvdsaddr  12548  dvdssub  12549  dvdssubr  12550  fzocongeq  12569  odd2np1  12584  opoe  12606  omoe  12607  opeo  12608  omeo  12609  divalgb  12636  ndvdsadd  12642  bitsfi  12668  gcdmndc  12676  gcdabs  12709  dvdsgcd  12733  absmulgcd  12738  gcdmultiple  12741  gcdmultiplez  12742  rpmulgcd  12747  sqgcd  12750  dvdssqlem  12751  dvdssq  12752  nninfctlemfo  12761  nn0seqcvgd  12763  ialgrlemconst  12765  algrf  12767  algrp1  12768  algcvg  12770  algcvga  12773  lcmval  12785  lcmabs  12798  lcmgcd  12800  lcmdvds  12801  lcmgcdnn  12804  coprmgcdb  12810  coprmdvds  12814  coprmdvds2  12815  qredeq  12818  isprm3  12840  nprm  12845  divgcdodd  12865  prmdvdsexp  12870  sqrt2irr  12884  zgcdsq  12923  hashdvds  12943  phiprmpw  12944  crth  12946  phimullem  12947  modprm0  12977  coprimeprodsq  12980  coprimeprodsq2  12981  pythagtriplem2  12989  pythagtriplem19  13005  pcdvdsb  13043  pcneg  13048  pc2dvds  13053  pc11  13054  pcmpt  13066  pcfac  13073  infpnlem1  13082  prmunb  13085  1arithlem4  13089  1arith  13090  gzaddcl  13100  gzmulcl  13101  gzreim  13102  gzsubcl  13103  4sqlem1  13111  4sqlem4a  13114  4sqlem4  13115  4sqlem12  13125  ballotfilemfc0  13176  ballotfilemfcc  13177  setsvalg  13326  setsfun0  13332  restval  13542  xpsval  13649  mndinvmod  13742  resmhm  13784  resmhm2  13785  mhmco  13787  dfgrp3m  13896  mhmmnd  13917  mulgnngsum  13928  mulgnn0z  13950  mulgnndir  13952  ghmex  14056  0ghm  14059  resghm  14061  resghm2  14062  ghmco  14065  ghmeql  14068  kerf1ghm  14075  ablsubsub23  14126  dfrhm2  14384  isrhm  14388  rhmfn  14402  rhmval  14403  rhmco  14404  resrhm  14479  rhmeql  14481  rhmima  14482  lmodfopne  14586  lspf  14649  znidom  14917  znrrg  14920  innei  15140  cnovex  15173  txuni2  15233  txbasex  15234  txbas  15235  txtop  15237  txtopon  15239  txss12  15243  txbasval  15244  txcnp  15248  upxp  15249  txcnmpt  15250  uptx  15251  txcn  15252  txrest  15253  txdis  15254  cnmpt21  15268  hmeoco  15293  txhmeo  15296  isxmet2d  15325  blin2  15409  comet  15476  metcn  15491  txmetcn  15496  qtopbasss  15498  qtopbas  15499  remetdval  15524  bl2ioo  15527  blssioo  15530  divcnap  15542  cncfmet  15569  dvaddxxbr  15678  dvcjbr  15685  plyf  15714  ply1termlem  15719  plymullem1  15725  plyaddlem  15726  plymullem  15727  plycolemc  15735  plyreres  15741  dvply1  15742  efle  15753  reapef  15755  sinperlem  15785  sincosq2sgn  15804  sincosq3sgn  15805  sincos6thpi  15819  ioocosf1o  15831  relogoprlem  15845  logleb  15852  cxple3  15898  cxpcom  15915  dvdsppwf1o  15969  fsumdvdsmul  15971  1sgmprm  15974  mersenne  15977  lgslem3  15987  lgsdir2  16018  lgsdir  16020  lgsdilem2  16021  lgsdi  16022  gausslemma2dlem1a  16043  gausslemma2dlem3  16048  gausslemma2dlem6  16052  lgseisenlem3  16057  lgseisenlem4  16058  lgsquadlem1  16062  lgsquadlem2  16063  lgsquad2  16068  lgsquad3  16069  2lgslem1a1  16071  2lgslem1a  16073  2lgslem1c  16075  2sqlem2  16100  mul2sq  16101  2sqlem7  16106  usgredg2v  16331  ushgredgedg  16333  ushgredgedgloop  16335  uhgrissubgr  16368  vtxedgfi  16396  vtxlpfi  16397  wlkeq  16461  uspgr2wlkeq  16472  clwwlkccatlem  16507  clwwlkccat  16508  clwwlknccat  16530  bj-inex  16789  bj-bdfindis  16829  triap  16925  cvgcmp2nlemabs  16928  trilpolemisumle  16934  inffz  16970