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  8467  cnegex  8468  resubcl  8554  subeqrev  8666  muladd  8675  mulsub  8692  mulsub2  8693  ltaddsub2  8729  leaddsub2  8731  leltadd  8739  ltaddpos2  8745  posdif  8747  addge02  8765  mullt0  8772  recexre  8870  recextlem1  8943  recexap  8945  divmuldivap  9006  conjmulap  9023  div2subap  9131  prodgt02  9147  prodge02  9149  lemul2  9151  lemul2a  9153  ltmulgt12  9159  lemulge12  9161  ltmuldiv2  9169  ltdivmul2  9172  ledivmul2  9174  lemuldiv2  9176  negiso  9249  cju  9255  peano5nni  9260  nnaddcl  9277  nnmulcl  9278  nnsub  9296  addltmul  9495  avgle1  9499  avgle2  9500  nnrecl  9514  nn0nnaddcl  9547  zsubcl  9638  zleloe  9644  znnsub  9649  nzadd  9650  zmulcl  9651  zltp1le  9652  zleltp1  9653  nnleltp1  9657  nnltp1le  9658  nnaddm1cl  9659  nn0ltp1le  9660  nn0leltp1  9661  nn0ltlem1  9662  znn0sub  9663  nn0sub  9664  elz2  9669  zapne  9672  zdcle  9674  zdclt  9675  zltlen  9677  nn0lem1lt  9682  nnlem1lt  9683  nnltlem1  9684  zdiv  9687  zextle  9690  zextlt  9691  btwnnz  9693  prime  9698  nneo  9702  peano2uz2  9706  peano5uzti  9707  uzind  9710  fzind  9714  fnn0ind  9715  uzneg  9894  uz11  9898  eluzp1m1  9899  eluzp1p1  9901  uzin  9908  indstr  9946  uz2mulcl  9961  qre  9978  qaddcl  9988  qsubcl  9991  qltlen  9993  qlttri2  9994  irradd  9999  elpqb  10003  cnref1o  10004  rpaddcl  10031  rpmulcl  10032  rpdivcl  10033  rexadd  10207  rexsub  10208  xaddcom  10216  xnn0xadd0  10222  xnegdi  10223  elicc2  10293  iccshftr  10349  iccshftl  10351  iccdil  10353  icccntr  10355  fzval2  10367  elfz1eq  10392  peano2fzr  10394  fznlem  10398  fzsplit2  10407  fzsplit3  10410  fzaddel  10417  fzsubel  10418  fzrev2  10444  fzrev3  10446  uzsplit  10451  fzrevral  10464  fzrevral3  10466  fzshftral  10467  elfz2nn0  10471  fznn0sub2  10487  fz0fzdiffz0  10489  elfzmlbp  10491  difelfzle  10493  difelfznle  10494  1fv  10498  elfzouz2  10521  fzo0n  10527  fzouzsplit  10540  fzoun  10542  elfzo0le  10549  fzonmapblen  10551  fzofzim  10552  fzoaddel2  10560  eluzgtdifelfzo  10567  elfzodifsumelfzo  10571  ubmelm1fzo  10596  fzofzp1b  10598  fzosplitprm1  10605  fzostep1  10608  subfzo0  10613  zsupcllemstep  10614  qdclt  10632  qbtwnxr  10644  flqbi2  10678  divfl0  10683  flqzadd  10685  flqmulnn0  10686  addmodidr  10762  modfzo0difsn  10784  frec2uzltd  10792  frec2uzrand  10794  frecfzen2  10816  seqshft2g  10871  seq3split  10877  seqsplitg  10878  seq3caopr2  10882  seqcaopr2g  10883  seqf1oglem2  10909  exp3vallem  10929  expcllem  10939  expcl2lemap  10940  1exp  10957  expge1  10965  expadd  10970  expmul  10973  expsubap  10976  leexp1a  10983  lt2sq  11002  le2sq  11003  sumsqeq0  11007  qsqeqor  11039  bernneq  11050  bernneq2  11051  sq11ap  11097  facdiv  11128  faclbnd  11131  faclbnd3  11133  faclbnd6  11134  facavg  11136  bcrpcl  11143  bccmpl  11144  bcm1n  11159  fiubm  11223  seq3coll  11242  eqwrd  11293  ccatcl  11309  ccatclab  11310  ccatlen  11311  ccat0  11312  ccatval1  11313  ccatval2  11314  elfzelfzccat  11316  ccatvalfn  11317  ccatsymb  11318  ccatval21sw  11321  ccatrn  11325  lswccatn0lsw  11327  ccatalpha  11329  ccatrcl1  11330  swrdfv2  11383  swrdsbslen  11386  swrdspsleq  11387  swrdccat2  11391  pfxclz  11399  ccatpfx  11421  pfxccat1  11422  swrdswrdlem  11424  pfxswrd  11426  pfxccatin12lem4  11446  pfxccatin12lem1  11448  pfxccatin12lem2  11451  pfxccatin12lem3  11452  pfxccat3  11454  swrdccat  11455  pfxccatpfx2  11457  pfxccat3a  11458  swrdccat3blem  11459  swrdccat3b  11460  s2dmg  11510  shftfvalg  11531  shftf  11543  crre  11570  crim  11571  mulreap  11577  readd  11582  resub  11583  remul2  11586  imadd  11590  imsub  11591  immul2  11593  ipcnval  11599  cjsub  11605  cjreim  11617  caucvgre  11695  rexanuz  11702  rexuz3  11704  resqrexlemover  11724  resqrexlemcvg  11733  resqrexlemglsq  11736  sqrtle  11750  sqrtlt  11751  sqrt11ap  11752  sqrt11  11753  absreimsq  11781  absreim  11782  absmul  11783  sqabs  11796  absdiflt  11806  absdifle  11807  abssuble0  11817  abs2difabs  11822  fzomaxdif  11827  caubnd2  11831  rpmaxcl  11937  zmaxcl  11938  nn0maxcl  11939  minmax  11944  mincl  11945  min1inf  11946  min2inf  11947  minabs  11950  minclpr  11951  rpmincl  11952  2zinfmin  11957  xrmaxrecl  11969  xrminmax  11979  xrmincl  11980  xrmin1inf  11981  xrmin2inf  11982  xrminrecl  11987  xrminrpcl  11988  iooinsup  11991  climconst2  12005  climuni  12007  2clim  12015  climshft  12018  climshft2  12020  cjcn2  12030  climaddc1  12043  climmulc2  12045  climsubc1  12046  climsubc2  12047  climlec2  12055  summodclem2a  12096  zsumdc  12099  isumclim3  12138  mptfzshft  12157  fsumrev  12158  fisum0diag2  12162  telfsumo2  12182  fsumparts  12185  cvgcmpub  12191  binomlem  12198  binom1p  12200  binom1dif  12202  bcxmas  12204  isumshft  12205  expcnvap0  12217  expcnv  12219  geosergap  12221  geolim  12226  cvgratnnlemrate  12245  mertenslemi1  12250  mertenslem2  12251  mertensabs  12252  prodmodc  12293  zproddc  12294  fprodf1o  12303  fprodeq0  12332  efcj  12388  eftlub  12405  effsumlt  12407  efieq  12450  sinsub  12455  cossub  12456  subsin  12458  sinmul  12459  cosmul  12460  addcos  12461  subcos  12462  dvdssub2  12550  dvdsadd  12551  dvdsaddr  12552  dvdssub  12553  dvdssubr  12554  fzocongeq  12573  odd2np1  12588  opoe  12610  omoe  12611  opeo  12612  omeo  12613  divalgb  12640  ndvdsadd  12646  bitsfi  12672  gcdmndc  12680  gcdabs  12713  dvdsgcd  12737  absmulgcd  12742  gcdmultiple  12745  gcdmultiplez  12746  rpmulgcd  12751  sqgcd  12754  dvdssqlem  12755  dvdssq  12756  nninfctlemfo  12765  nn0seqcvgd  12767  ialgrlemconst  12769  algrf  12771  algrp1  12772  algcvg  12774  algcvga  12777  lcmval  12789  lcmabs  12802  lcmgcd  12804  lcmdvds  12805  lcmgcdnn  12808  coprmgcdb  12814  coprmdvds  12818  coprmdvds2  12819  qredeq  12822  isprm3  12844  nprm  12849  divgcdodd  12869  prmdvdsexp  12874  sqrt2irr  12888  zgcdsq  12927  hashdvds  12947  phiprmpw  12948  crth  12950  phimullem  12951  modprm0  12981  coprimeprodsq  12984  coprimeprodsq2  12985  pythagtriplem2  12993  pythagtriplem19  13009  pcdvdsb  13047  pcneg  13052  pc2dvds  13057  pc11  13058  pcmpt  13070  pcfac  13077  infpnlem1  13086  prmunb  13089  1arithlem4  13093  1arith  13094  gzaddcl  13104  gzmulcl  13105  gzreim  13106  gzsubcl  13107  4sqlem1  13115  4sqlem4a  13118  4sqlem4  13119  4sqlem12  13129  ballotfilemfc0  13180  ballotfilemfcc  13181  setsvalg  13330  setsfun0  13336  restval  13546  mndinvmod  13710  resmhm  13746  resmhm2  13747  mhmco  13749  dfgrp3m  13858  mhmmnd  13873  mulgnngsum  13884  mulgnn0z  13906  mulgnndir  13908  ghmex  14012  0ghm  14015  resghm  14017  resghm2  14018  ghmco  14021  ghmeql  14024  kerf1ghm  14031  ablsubsub23  14082  xpsval  14147  dfrhm2  14403  isrhm  14407  rhmfn  14421  rhmval  14422  rhmco  14423  resrhm  14498  rhmeql  14500  rhmima  14501  lmodfopne  14604  lspf  14667  znidom  14935  znrrg  14938  innei  15158  cnovex  15191  txuni2  15251  txbasex  15252  txbas  15253  txtop  15255  txtopon  15257  txss12  15261  txbasval  15262  txcnp  15266  upxp  15267  txcnmpt  15268  uptx  15269  txcn  15270  txrest  15271  txdis  15272  cnmpt21  15286  hmeoco  15311  txhmeo  15314  isxmet2d  15343  blin2  15427  comet  15494  metcn  15509  txmetcn  15514  qtopbasss  15516  qtopbas  15517  remetdval  15542  bl2ioo  15545  blssioo  15548  divcnap  15560  cncfmet  15587  dvaddxxbr  15696  dvcjbr  15703  plyf  15732  ply1termlem  15737  plymullem1  15743  plyaddlem  15744  plymullem  15745  plycolemc  15753  plyreres  15759  dvply1  15760  efle  15771  reapef  15773  sinperlem  15803  sincosq2sgn  15822  sincosq3sgn  15823  sincos6thpi  15837  ioocosf1o  15849  relogoprlem  15863  logleb  15870  cxple3  15916  cxpcom  15933  dvdsppwf1o  15987  fsumdvdsmul  15989  1sgmprm  15992  mersenne  15995  lgslem3  16005  lgsdir2  16036  lgsdir  16038  lgsdilem2  16039  lgsdi  16040  gausslemma2dlem1a  16061  gausslemma2dlem3  16066  gausslemma2dlem6  16070  lgseisenlem3  16075  lgseisenlem4  16076  lgsquadlem1  16080  lgsquadlem2  16081  lgsquad2  16086  lgsquad3  16087  2lgslem1a1  16089  2lgslem1a  16091  2lgslem1c  16093  2sqlem2  16118  mul2sq  16119  2sqlem7  16124  usgredg2v  16349  ushgredgedg  16351  ushgredgedgloop  16353  uhgrissubgr  16386  vtxedgfi  16414  vtxlpfi  16415  wlkeq  16479  uspgr2wlkeq  16490  clwwlkccatlem  16525  clwwlkccat  16526  clwwlknccat  16548  bj-inex  16817  bj-bdfindis  16857  triap  16953  cvgcmp2nlemabs  16956  trilpolemisumle  16962  inffz  16997