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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  syl2anr  290  anim12i  338  syl2an2  602  syl2an2r  603  orandc  952  mp3an3an  1384  eqeqan12d  2254  sylan9eq  2291  csbcomg  3170  sylan9ss  3261  ssconb  3362  ineqan12d  3434  dfopg  3902  breqan12d  4146  opexg  4368  copsex2g  4386  ordin  4530  onin  4531  unexg  4589  eusv1  4598  opelvvg  4824  opthprc  4826  opbrop  4854  relop  4930  dmpropg  5260  unixpm  5323  funssres  5420  funinsn  5430  funtp  5434  fnco  5491  resasplitss  5569  fodmrnu  5623  relrnfvex  5713  funopdmsn  5895  fconst2g  5930  oveqan12d  6104  ovi3  6226  ovg  6228  f1opw2  6296  off  6315  offres  6368  suppfnss  6497  iunon  6555  nnsucsssuc  6765  nnaword1  6786  ertr  6822  erex  6831  brecop  6899  ecovdi  6920  ecovidi  6921  mapvalg  6932  pmvalg  6933  pmss12g  6956  mapsn  6972  en2sn  7102  xpf1o  7144  xpen  7145  phplem4  7156  ssfilem  7177  ssfilemd  7179  diffitest  7191  en1eqsn  7265  sbthlem7  7280  fsuppxpfi  7296  ordiso  7377  updjud  7423  fodju0  7488  finnum  7529  pr2nelem  7538  djucomen  7573  exmidontriimlem1  7578  2onetap  7622  ltsopi  7688  pitric  7689  pitri3or  7690  ltdcpi  7691  mulclpi  7696  addcompig  7697  mulcompig  7699  distrpig  7701  ltexpi  7705  ltapig  7706  ltmpig  7707  dfplpq2  7722  dfmpq2  7723  enqbreq2  7725  enqdc  7729  addcmpblnq  7735  addpipqqslem  7737  mulpipq2  7739  mulpipq  7740  mulpipqqs  7741  addclnq  7743  distrnqg  7755  ltdcnq  7765  ltrnqg  7788  enq0breq  7804  addclnq0  7819  nqnq0a  7822  nqnq0m  7823  nq0m0r  7824  distrnq0  7827  mulcomnq0  7828  genipv  7877  genplt2i  7878  genpelvl  7880  genpelvu  7881  addnqprlemrl  7925  addnqprlemru  7926  addnqprlemfl  7927  addnqprlemfu  7928  addnqpr  7929  mulnqprlemrl  7941  mulnqprlemru  7942  mulnqprlemfl  7943  mulnqprlemfu  7944  mulnqpr  7945  distrlem4prl  7952  distrlem4pru  7953  ltnqpr  7961  recexprlemloc  7999  archrecnq  8031  mulclsr  8122  1idsr  8136  00sr  8137  prsradd  8154  axmulass  8241  axdistr  8242  axcnre  8249  peano5nnnn  8260  mulrid  8324  axltadd  8396  lenlt  8402  cnegexlem3  8505  cnegex  8506  resubcl  8592  subeqrev  8704  muladd  8713  mulsub  8730  mulsub2  8731  ltaddsub2  8767  leaddsub2  8769  leltadd  8777  ltaddpos2  8783  posdif  8785  addge02  8803  mullt0  8810  recexre  8909  recextlem1  8982  recexap  8984  divmuldivap  9045  conjmulap  9062  div2subap  9170  prodgt02  9186  prodge02  9188  lemul2  9190  lemul2a  9192  ltmulgt12  9198  lemulge12  9200  ltmuldiv2  9208  ltdivmul2  9211  ledivmul2  9213  lemuldiv2  9215  negiso  9288  cju  9294  peano5nni  9310  nnaddcl  9327  nnmulcl  9328  nnsub  9346  addltmul  9547  avgle1  9551  avgle2  9552  nnrecl  9566  nn0nnaddcl  9599  zsubcl  9690  zleloe  9696  znnsub  9701  nzadd  9702  zmulcl  9703  zltp1le  9704  zleltp1  9705  nnleltp1  9709  nnltp1le  9710  nnaddm1cl  9711  nn0ltp1le  9712  nn0leltp1  9713  nn0ltlem1  9714  znn0sub  9715  nn0sub  9716  elz2  9721  zapne  9724  zdcle  9726  zdclt  9727  zltlen  9729  nn0lem1lt  9734  nnlem1lt  9735  nnltlem1  9736  zdiv  9739  zextle  9742  zextlt  9743  btwnnz  9745  prime  9750  nneo  9754  peano2uz2  9758  peano5uzti  9759  uzind  9762  fzind  9766  fnn0ind  9767  uzneg  9951  uz11  9955  eluzp1m1  9956  eluzp1p1  9958  uzin  9965  indstr  10003  uz2mulcl  10018  qre  10035  qaddcl  10045  qsubcl  10048  qltlen  10050  qlttri2  10051  irradd  10056  elpqb  10061  cnref1o  10062  rpaddcl  10089  rpmulcl  10090  rpdivcl  10091  rexadd  10265  rexsub  10266  xaddcom  10274  xnn0xadd0  10280  xnegdi  10281  elicc2  10351  iccshftr  10407  iccshftl  10409  iccdil  10411  icccntr  10413  fzval2  10425  elfz1eq  10450  peano2fzr  10452  fznlem  10456  fzsplit2  10466  fzsplit3  10469  fzaddel  10476  fzsubel  10477  fzrev2  10503  fzrev3  10505  uzsplit  10510  fzrevral  10523  fzrevral3  10525  fzshftral  10526  elfz2nn0  10530  fznn0sub2  10546  fz0fzdiffz0  10548  elfzmlbp  10550  difelfzle  10552  difelfznle  10553  1fv  10557  elfzouz2  10580  fzo0n  10586  fzouzsplit  10599  fzoun  10601  elfzo0le  10608  fzonmapblen  10610  fzofzim  10611  fzoaddel2  10619  eluzgtdifelfzo  10626  elfzodifsumelfzo  10630  ubmelm1fzo  10655  fzofzp1b  10657  fzosplitprm1  10664  fzostep1  10667  subfzo0  10672  zsupcllemstep  10673  qdclt  10691  qbtwnxr  10703  flqbi2  10740  divfl0  10745  flqzadd  10747  flqmulnn0  10748  addmodidr  10824  modfzo0difsn  10846  frec2uzltd  10854  frec2uzrand  10856  frecfzen2  10878  seqshft2g  10933  seq3split  10939  seqsplitg  10940  seq3caopr2  10944  seqcaopr2g  10945  seqf1oglem2  10971  exp3vallem  10991  expcllem  11001  expcl2lemap  11002  1exp  11019  expge1  11027  expadd  11032  expmul  11035  expsubap  11038  leexp1a  11045  lt2sq  11064  le2sq  11065  sumsqeq0  11069  qsqeqor  11101  bernneq  11112  bernneq2  11113  sq11ap  11159  facdiv  11191  faclbnd  11194  faclbnd3  11196  faclbnd6  11197  facavg  11199  bcrpcl  11206  bccmpl  11207  bcm1n  11222  fiubm  11286  seq3coll  11309  eqwrd  11360  ccatcl  11376  ccatclab  11377  ccatlen  11378  ccat0  11379  ccatval1  11380  ccatval2  11381  elfzelfzccat  11383  ccatvalfn  11384  ccatsymb  11385  ccatval21sw  11388  ccatrn  11392  lswccatn0lsw  11394  ccatalpha  11396  ccatrcl1  11397  swrdfv2  11450  swrdsbslen  11453  swrdspsleq  11454  swrdccat2  11458  pfxclz  11466  ccatpfx  11488  pfxccat1  11489  swrdswrdlem  11491  pfxswrd  11493  pfxccatin12lem4  11513  pfxccatin12lem1  11515  pfxccatin12lem2  11518  pfxccatin12lem3  11519  pfxccat3  11521  swrdccat  11522  pfxccatpfx2  11524  pfxccat3a  11525  swrdccat3blem  11526  swrdccat3b  11527  s2dmg  11577  shftfvalg  11598  shftf  11610  crre  11637  crim  11638  mulreap  11644  readd  11649  resub  11650  remul2  11653  imadd  11657  imsub  11658  immul2  11660  ipcnval  11666  cjsub  11672  cjreim  11684  caucvgre  11762  rexanuz  11769  rexuz3  11771  resqrexlemover  11791  resqrexlemcvg  11800  resqrexlemglsq  11803  sqrtle  11817  sqrtlt  11818  sqrt11ap  11819  sqrt11  11820  absreimsq  11848  absreim  11849  absmul  11850  sqabs  11864  absdiflt  11874  absdifle  11875  abssuble0  11885  abs2difabs  11890  fzomaxdif  11895  caubnd2  11899  rpmaxcl  12005  zmaxcl  12006  nn0maxcl  12007  minmax  12013  mincl  12014  min1inf  12015  min2inf  12016  minabs  12019  minclpr  12020  rpmincl  12021  zmincl  12022  2zinfmin  12027  xrmaxrecl  12039  xrminmax  12049  xrmincl  12050  xrmin1inf  12051  xrmin2inf  12052  xrminrecl  12057  xrminrpcl  12058  iooinsup  12061  climconst2  12075  climuni  12077  2clim  12085  climshft  12088  climshft2  12090  cjcn2  12100  climaddc1  12113  climmulc2  12115  climsubc1  12116  climsubc2  12117  climlec2  12125  summodclem2a  12166  zsumdc  12169  isumclim3  12208  mptfzshft  12227  fsumrev  12228  fisum0diag2  12232  telfsumo2  12252  fsumparts  12255  cvgcmpub  12261  binomlem  12268  binom1p  12270  binom1dif  12272  bcxmas  12274  isumshft  12275  expcnvap0  12287  expcnv  12289  geosergap  12291  geolim  12296  cvgratnnlemrate  12315  mertenslemi1  12320  mertenslem2  12321  mertensabs  12322  prodmodc  12363  zproddc  12364  fprodf1o  12373  fprodeq0  12402  efcj  12458  eftlub  12475  effsumlt  12477  efieq  12520  sinsub  12525  cossub  12526  subsin  12528  sinmul  12529  cosmul  12530  addcos  12531  subcos  12532  dvdssub2  12620  dvdsadd  12621  dvdsaddr  12622  dvdssub  12623  dvdssubr  12624  fzocongeq  12643  odd2np1  12658  opoe  12680  omoe  12681  opeo  12682  omeo  12683  divalgb  12710  ndvdsadd  12716  bitsfi  12742  gcdmndc  12750  gcdabs  12783  dvdsgcd  12807  absmulgcd  12812  gcdmultiple  12815  gcdmultiplez  12816  rpmulgcd  12821  sqgcd  12824  dvdssqlem  12825  dvdssq  12826  nninfctlemfo  12835  nn0seqcvgd  12837  ialgrlemconst  12839  algrf  12841  algrp1  12842  algcvg  12844  algcvga  12847  lcmval  12859  lcmabs  12872  lcmgcd  12874  lcmdvds  12875  lcmgcdnn  12878  coprmgcdb  12884  coprmdvds  12888  coprmdvds2  12889  qredeq  12892  isprm3  12914  nprm  12919  divgcdodd  12940  prmdvdsexp  12945  sqrt2irr  12959  zgcdsq  12999  hashdvds  13021  phiprmpw  13022  crth  13024  phimullem  13025  modprm0  13055  coprimeprodsq  13058  coprimeprodsq2  13059  pythagtriplem2  13067  pythagtriplem19  13083  pcdvdsb  13121  pcneg  13126  pc2dvds  13131  pc11  13132  pcmpt  13144  pcfac  13151  infpnlem1  13160  prmunb  13163  1arithlem4  13167  1arith  13168  gzaddcl  13178  gzmulcl  13179  gzreim  13180  gzsubcl  13181  4sqlem1  13189  4sqlem4a  13192  4sqlem4  13193  4sqlem12  13203  ballotfilemfc0  13283  ballotfilemfcc  13284  setsvalg  13433  setsfun0  13439  restval  13650  mndinvmod  13809  resmhm  13845  resmhm2  13846  mhmco  13848  dfgrp3m  13955  mhmmnd  13970  mulgnngzsum  13981  mulgnn0z  14003  mulgnndir  14005  ghmex  14109  0ghm  14112  resghm  14114  resghm2  14115  ghmco  14118  ghmeql  14121  kerf1ghm  14128  ablsubsub23  14180  xpsval  14252  dfrhm2  14512  isrhm  14516  rhmfn  14530  rhmval  14531  rhmco  14532  resrhm  14607  rhmeql  14609  rhmima  14610  lmodfopne  14714  lspf  14777  znidom  15043  znrrg  15046  issubassa3  15063  innei  15316  cnovex  15349  txuni2  15409  txbasex  15410  txbas  15411  txtop  15413  txtopon  15415  txss12  15419  txbasval  15420  txcnp  15424  upxp  15425  txcnmpt  15426  uptx  15427  txcn  15428  txrest  15429  txdis  15430  cnmpt21  15444  hmeoco  15469  txhmeo  15472  isxmet2d  15501  blin2  15585  comet  15652  metcn  15667  txmetcn  15672  qtopbasss  15674  qtopbas  15675  remetdval  15700  bl2ioo  15703  blssioo  15706  divcnap  15718  cncfmet  15745  dvaddxxbr  15854  dvcjbr  15861  plyf  15890  ply1termlem  15895  plymullem1  15901  plyaddlem  15902  plymullem  15903  plycolemc  15911  plyreres  15917  dvply1  15918  efle  15929  reapef  15931  sinperlem  15962  sincosq2sgn  15981  sincosq3sgn  15982  sincos6thpi  15996  ioocosf1o  16008  reaplog  16022  relogoprlem  16023  logleb  16030  cxple3  16079  cxpcom  16096  birthdaylem2  16148  birthdaylem3  16149  dvdsppwf1o  16205  fsumdvdsmul  16207  1sgmprm  16210  chtublem  16217  mersenne  16219  pcbcctr  16225  bcmono  16226  bposlem1  16233  bposlem2  16234  bposlem3  16235  bposlem5  16237  lgslem3  16243  lgsdir2  16274  lgsdir  16276  lgsdilem2  16277  lgsdi  16278  gausslemma2dlem1a  16299  gausslemma2dlem3  16304  gausslemma2dlem6  16308  lgseisenlem3  16313  lgseisenlem4  16314  lgsquadlem1  16318  lgsquadlem2  16319  lgsquad2  16324  lgsquad3  16325  2lgslem1a1  16327  2lgslem1a  16329  2lgslem1c  16331  2sqlem2  16356  mul2sq  16357  2sqlem7  16362  usgredg2v  16587  ushgredgedg  16589  ushgredgedgloop  16591  uhgrissubgr  16624  vtxedgfi  16652  vtxlpfi  16653  wlkeq  16717  uspgr2wlkeq  16728  clwwlkccatlem  16763  clwwlkccat  16764  clwwlknccat  16786  bj-inex  17055  bj-bdfindis  17095  triap  17200  cvgcmp2nlemabs  17203  trilpolemisumle  17209  inffz  17244