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  596  syl2an2r  597  orandc  945  mp3an3an  1377  eqeqan12d  2245  sylan9eq  2282  csbcomg  3147  sylan9ss  3237  ssconb  3337  ineqan12d  3407  dfopg  3854  breqan12d  4098  opexg  4313  copsex2g  4331  ordin  4473  onin  4474  unexg  4531  eusv1  4540  opelvvg  4765  opthprc  4767  opbrop  4795  relop  4869  dmpropg  5197  unixpm  5260  funssres  5356  funinsn  5366  funtp  5370  fnco  5427  resasplitss  5501  fodmrnu  5552  relrnfvex  5641  funopdmsn  5812  fconst2g  5847  oveqan12d  6013  ovi3  6133  ovg  6135  f1opw2  6202  off  6221  offres  6270  iunon  6420  nnsucsssuc  6628  nnaword1  6649  ertr  6685  erex  6694  brecop  6762  ecovdi  6783  ecovidi  6784  mapvalg  6795  pmvalg  6796  pmss12g  6812  mapsn  6827  en2sn  6956  xpf1o  6993  xpen  6994  phplem4  7004  ssfilem  7025  diffitest  7037  en1eqsn  7103  sbthlem7  7118  ordiso  7191  updjud  7237  fodju0  7302  finnum  7343  pr2nelem  7352  djucomen  7386  exmidontriimlem1  7391  2onetap  7429  ltsopi  7495  pitric  7496  pitri3or  7497  ltdcpi  7498  mulclpi  7503  addcompig  7504  mulcompig  7506  distrpig  7508  ltexpi  7512  ltapig  7513  ltmpig  7514  dfplpq2  7529  dfmpq2  7530  enqbreq2  7532  enqdc  7536  addcmpblnq  7542  addpipqqslem  7544  mulpipq2  7546  mulpipq  7547  mulpipqqs  7548  addclnq  7550  distrnqg  7562  ltdcnq  7572  ltrnqg  7595  enq0breq  7611  addclnq0  7626  nqnq0a  7629  nqnq0m  7630  nq0m0r  7631  distrnq0  7634  mulcomnq0  7635  genipv  7684  genplt2i  7685  genpelvl  7687  genpelvu  7688  addnqprlemrl  7732  addnqprlemru  7733  addnqprlemfl  7734  addnqprlemfu  7735  addnqpr  7736  mulnqprlemrl  7748  mulnqprlemru  7749  mulnqprlemfl  7750  mulnqprlemfu  7751  mulnqpr  7752  distrlem4prl  7759  distrlem4pru  7760  ltnqpr  7768  recexprlemloc  7806  archrecnq  7838  mulclsr  7929  1idsr  7943  00sr  7944  prsradd  7961  axmulass  8048  axdistr  8049  axcnre  8056  peano5nnnn  8067  mulrid  8131  axltadd  8204  lenlt  8210  cnegexlem3  8311  cnegex  8312  resubcl  8398  subeqrev  8510  muladd  8518  mulsub  8535  mulsub2  8536  ltaddsub2  8572  leaddsub2  8574  leltadd  8582  ltaddpos2  8588  posdif  8590  addge02  8608  mullt0  8615  recexre  8713  recextlem1  8786  recexap  8788  divmuldivap  8847  conjmulap  8864  div2subap  8972  prodgt02  8988  prodge02  8990  lemul2  8992  lemul2a  8994  ltmulgt12  9000  lemulge12  9002  ltmuldiv2  9010  ltdivmul2  9013  ledivmul2  9015  lemuldiv2  9017  negiso  9090  cju  9096  peano5nni  9101  nnaddcl  9118  nnmulcl  9119  nnsub  9137  addltmul  9336  avgle1  9340  avgle2  9341  nnrecl  9355  nn0nnaddcl  9388  zsubcl  9475  zleloe  9481  znnsub  9486  nzadd  9487  zmulcl  9488  zltp1le  9489  zleltp1  9490  nnleltp1  9494  nnltp1le  9495  nnaddm1cl  9496  nn0ltp1le  9497  nn0leltp1  9498  nn0ltlem1  9499  znn0sub  9500  nn0sub  9501  elz2  9506  zapne  9509  zdcle  9511  zdclt  9512  zltlen  9513  nn0lem1lt  9518  nnlem1lt  9519  nnltlem1  9520  zdiv  9523  zextle  9526  zextlt  9527  btwnnz  9529  prime  9534  nneo  9538  peano2uz2  9542  peano5uzti  9543  uzind  9546  fzind  9550  fnn0ind  9551  uzneg  9729  uz11  9733  eluzp1m1  9734  eluzp1p1  9736  uzin  9743  indstr  9776  uz2mulcl  9791  qre  9808  qaddcl  9818  qsubcl  9821  qltlen  9823  qlttri2  9824  irradd  9829  elpqb  9833  cnref1o  9834  rpaddcl  9861  rpmulcl  9862  rpdivcl  9863  rexadd  10036  rexsub  10037  xaddcom  10045  xnn0xadd0  10051  xnegdi  10052  elicc2  10122  iccshftr  10178  iccshftl  10180  iccdil  10182  icccntr  10184  fzval2  10195  elfz1eq  10219  peano2fzr  10221  fznlem  10225  fzsplit2  10234  fzaddel  10243  fzsubel  10244  fzrev2  10269  fzrev3  10271  uzsplit  10276  fzrevral  10289  fzrevral3  10291  fzshftral  10292  elfz2nn0  10296  fznn0sub2  10312  fz0fzdiffz0  10314  elfzmlbp  10316  difelfzle  10318  difelfznle  10319  1fv  10323  elfzouz2  10346  fzo0n  10352  fzouzsplit  10365  fzoun  10367  elfzo0le  10373  fzonmapblen  10375  fzofzim  10376  fzoaddel2  10383  eluzgtdifelfzo  10390  elfzodifsumelfzo  10394  ubmelm1fzo  10419  fzofzp1b  10421  fzosplitprm1  10427  fzostep1  10430  subfzo0  10435  zsupcllemstep  10436  qdclt  10452  qbtwnxr  10464  flqbi2  10498  divfl0  10503  flqzadd  10505  flqmulnn0  10506  addmodidr  10582  modfzo0difsn  10604  frec2uzltd  10612  frec2uzrand  10614  frecfzen2  10636  seqshft2g  10691  seq3split  10697  seqsplitg  10698  seq3caopr2  10702  seqcaopr2g  10703  seqf1oglem2  10729  exp3vallem  10749  expcllem  10759  expcl2lemap  10760  1exp  10777  expge1  10785  expadd  10790  expmul  10793  expsubap  10796  leexp1a  10803  lt2sq  10822  le2sq  10823  sumsqeq0  10827  qsqeqor  10859  bernneq  10869  bernneq2  10870  sq11ap  10916  facdiv  10947  faclbnd  10950  faclbnd3  10952  faclbnd6  10953  facavg  10955  bcrpcl  10962  bccmpl  10963  fiubm  11037  seq3coll  11051  eqwrd  11098  ccatcl  11114  ccatclab  11115  ccatlen  11116  ccat0  11117  ccatval1  11118  ccatval2  11119  elfzelfzccat  11121  ccatvalfn  11122  ccatsymb  11123  ccatval21sw  11126  ccatrn  11130  lswccatn0lsw  11132  swrdfv2  11181  swrdsbslen  11184  swrdspsleq  11185  swrdccat2  11189  pfxclz  11197  ccatpfx  11219  pfxccat1  11220  swrdswrdlem  11222  pfxswrd  11224  pfxccatin12lem4  11244  pfxccatin12lem1  11246  pfxccatin12lem2  11249  pfxccatin12lem3  11250  pfxccat3  11252  swrdccat  11253  pfxccatpfx2  11255  pfxccat3a  11256  swrdccat3blem  11257  swrdccat3b  11258  s2dmg  11308  shftfvalg  11315  shftf  11327  crre  11354  crim  11355  mulreap  11361  readd  11366  resub  11367  remul2  11370  imadd  11374  imsub  11375  immul2  11377  ipcnval  11383  cjsub  11389  cjreim  11400  caucvgre  11478  rexanuz  11485  rexuz3  11487  resqrexlemover  11507  resqrexlemcvg  11516  resqrexlemglsq  11519  sqrtle  11533  sqrtlt  11534  sqrt11ap  11535  sqrt11  11536  absreimsq  11564  absreim  11565  absmul  11566  sqabs  11579  absdiflt  11589  absdifle  11590  abssuble0  11600  abs2difabs  11605  fzomaxdif  11610  caubnd2  11614  rpmaxcl  11720  zmaxcl  11721  nn0maxcl  11722  minmax  11727  mincl  11728  min1inf  11729  min2inf  11730  minabs  11733  minclpr  11734  rpmincl  11735  2zinfmin  11740  xrmaxrecl  11752  xrminmax  11762  xrmincl  11763  xrmin1inf  11764  xrmin2inf  11765  xrminrecl  11770  xrminrpcl  11771  iooinsup  11774  climconst2  11788  climuni  11790  2clim  11798  climshft  11801  climshft2  11803  cjcn2  11813  climaddc1  11826  climmulc2  11828  climsubc1  11829  climsubc2  11830  climlec2  11838  summodclem2a  11878  zsumdc  11881  isumclim3  11920  mptfzshft  11939  fsumrev  11940  fisum0diag2  11944  telfsumo2  11964  fsumparts  11967  cvgcmpub  11973  binomlem  11980  binom1p  11982  binom1dif  11984  bcxmas  11986  isumshft  11987  expcnvap0  11999  expcnv  12001  geosergap  12003  geolim  12008  cvgratnnlemrate  12027  mertenslemi1  12032  mertenslem2  12033  mertensabs  12034  prodmodc  12075  zproddc  12076  fprodf1o  12085  fprodeq0  12114  efcj  12170  eftlub  12187  effsumlt  12189  efieq  12232  sinsub  12237  cossub  12238  subsin  12240  sinmul  12241  cosmul  12242  addcos  12243  subcos  12244  dvdssub2  12332  dvdsadd  12333  dvdsaddr  12334  dvdssub  12335  dvdssubr  12336  fzocongeq  12355  odd2np1  12370  opoe  12392  omoe  12393  opeo  12394  omeo  12395  divalgb  12422  ndvdsadd  12428  bitsfi  12454  gcdmndc  12462  gcdabs  12495  dvdsgcd  12519  absmulgcd  12524  gcdmultiple  12527  gcdmultiplez  12528  rpmulgcd  12533  sqgcd  12536  dvdssqlem  12537  dvdssq  12538  nninfctlemfo  12547  nn0seqcvgd  12549  ialgrlemconst  12551  algrf  12553  algrp1  12554  algcvg  12556  algcvga  12559  lcmval  12571  lcmabs  12584  lcmgcd  12586  lcmdvds  12587  lcmgcdnn  12590  coprmgcdb  12596  coprmdvds  12600  coprmdvds2  12601  qredeq  12604  isprm3  12626  nprm  12631  divgcdodd  12651  prmdvdsexp  12656  sqrt2irr  12670  zgcdsq  12709  hashdvds  12729  phiprmpw  12730  crth  12732  phimullem  12733  modprm0  12763  coprimeprodsq  12766  coprimeprodsq2  12767  pythagtriplem2  12775  pythagtriplem19  12791  pcdvdsb  12829  pcneg  12834  pc2dvds  12839  pc11  12840  pcmpt  12852  pcfac  12859  infpnlem1  12868  prmunb  12871  1arithlem4  12875  1arith  12876  gzaddcl  12886  gzmulcl  12887  gzreim  12888  gzsubcl  12889  4sqlem1  12897  4sqlem4a  12900  4sqlem4  12901  4sqlem12  12911  setsvalg  13048  setsfun0  13054  restval  13264  xpsval  13371  mndinvmod  13464  resmhm  13506  resmhm2  13507  mhmco  13509  dfgrp3m  13618  mhmmnd  13639  mulgnngsum  13650  mulgnn0z  13672  mulgnndir  13674  ghmex  13778  0ghm  13781  resghm  13783  resghm2  13784  ghmco  13787  ghmeql  13790  kerf1ghm  13797  ablsubsub23  13848  dfrhm2  14103  isrhm  14107  rhmfn  14121  rhmval  14122  rhmco  14123  resrhm  14197  rhmeql  14199  rhmima  14200  lmodfopne  14275  lspf  14338  znidom  14606  znrrg  14609  innei  14822  cnovex  14855  txuni2  14915  txbasex  14916  txbas  14917  txtop  14919  txtopon  14921  txss12  14925  txbasval  14926  txcnp  14930  upxp  14931  txcnmpt  14932  uptx  14933  txcn  14934  txrest  14935  txdis  14936  cnmpt21  14950  hmeoco  14975  txhmeo  14978  isxmet2d  15007  blin2  15091  comet  15158  metcn  15173  txmetcn  15178  qtopbasss  15180  qtopbas  15181  remetdval  15206  bl2ioo  15209  blssioo  15212  divcnap  15224  cncfmet  15251  dvaddxxbr  15360  dvcjbr  15367  plyf  15396  ply1termlem  15401  plymullem1  15407  plyaddlem  15408  plymullem  15409  plycolemc  15417  plyreres  15423  dvply1  15424  efle  15435  reapef  15437  sinperlem  15467  sincosq2sgn  15486  sincosq3sgn  15487  sincos6thpi  15501  ioocosf1o  15513  relogoprlem  15527  logleb  15534  cxple3  15580  cxpcom  15597  dvdsppwf1o  15648  fsumdvdsmul  15650  1sgmprm  15653  mersenne  15656  lgslem3  15666  lgsdir2  15697  lgsdir  15699  lgsdilem2  15700  lgsdi  15701  gausslemma2dlem1a  15722  gausslemma2dlem3  15727  gausslemma2dlem6  15731  lgseisenlem3  15736  lgseisenlem4  15737  lgsquadlem1  15741  lgsquadlem2  15742  lgsquad2  15747  lgsquad3  15748  2lgslem1a1  15750  2lgslem1a  15752  2lgslem1c  15754  2sqlem2  15779  mul2sq  15780  2sqlem7  15785  usgredg2v  16007  ushgredgedg  16009  ushgredgedgloop  16011  bj-inex  16200  bj-bdfindis  16240  triap  16328  cvgcmp2nlemabs  16331  trilpolemisumle  16337  inffz  16371