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  4147  opexg  4370  copsex2g  4388  ordin  4532  onin  4533  unexg  4591  eusv1  4600  opelvvg  4826  opthprc  4828  opbrop  4856  relop  4932  dmpropg  5263  unixpm  5326  funssres  5423  funinsn  5433  funtp  5437  fnco  5494  resasplitss  5572  fodmrnu  5626  relrnfvex  5716  funopdmsn  5898  fconst2g  5933  oveqan12d  6107  ovi3  6229  ovg  6231  f1opw2  6299  off  6319  offres  6372  suppfnss  6501  iunon  6560  nnsucsssuc  6770  nnaword1  6791  ertr  6827  erex  6836  brecop  6904  ecovdi  6925  ecovidi  6926  mapvalg  6937  pmvalg  6938  pmss12g  6961  mapsn  6978  en2sn  7108  xpf1o  7150  xpen  7151  phplem4  7162  ssfilem  7183  ssfilemd  7185  diffitest  7197  en1eqsn  7272  sbthlem7  7287  ordiso  7382  updjud  7428  fodju0  7493  finnum  7534  pr2nelem  7543  djucomen  7578  exmidontriimlem1  7583  2onetap  7627  ltsopi  7693  pitric  7694  pitri3or  7695  ltdcpi  7696  mulclpi  7701  addcompig  7702  mulcompig  7704  distrpig  7706  ltexpi  7710  ltapig  7711  ltmpig  7712  dfplpq2  7727  dfmpq2  7728  enqbreq2  7730  enqdc  7734  addcmpblnq  7740  addpipqqslem  7742  mulpipq2  7744  mulpipq  7745  mulpipqqs  7746  addclnq  7748  distrnqg  7760  ltdcnq  7770  ltrnqg  7793  enq0breq  7809  addclnq0  7824  nqnq0a  7827  nqnq0m  7828  nq0m0r  7829  distrnq0  7832  mulcomnq0  7833  genipv  7882  genplt2i  7883  genpelvl  7885  genpelvu  7886  addnqprlemrl  7930  addnqprlemru  7931  addnqprlemfl  7932  addnqprlemfu  7933  addnqpr  7934  mulnqprlemrl  7946  mulnqprlemru  7947  mulnqprlemfl  7948  mulnqprlemfu  7949  mulnqpr  7950  distrlem4prl  7957  distrlem4pru  7958  ltnqpr  7966  recexprlemloc  8004  archrecnq  8036  mulclsr  8127  1idsr  8141  00sr  8142  prsradd  8159  axmulass  8246  axdistr  8247  axcnre  8254  peano5nnnn  8265  mulrid  8329  axltadd  8401  lenlt  8407  cnegexlem3  8510  cnegex  8511  resubcl  8597  subeqrev  8709  muladd  8718  mulsub  8735  mulsub2  8736  ltaddsub2  8772  leaddsub2  8774  leltadd  8782  ltaddpos2  8788  posdif  8790  addge02  8808  mullt0  8815  recexre  8914  recextlem1  8987  recexap  8989  divmuldivap  9050  conjmulap  9067  div2subap  9175  prodgt02  9191  prodge02  9193  lemul2  9195  lemul2a  9197  ltmulgt12  9203  lemulge12  9205  ltmuldiv2  9213  ltdivmul2  9216  ledivmul2  9218  lemuldiv2  9220  negiso  9293  cju  9299  peano5nni  9316  nnaddcl  9333  nnmulcl  9334  nnsub  9352  addltmul  9553  avgle1  9557  avgle2  9558  nnrecl  9572  nn0nnaddcl  9605  zsubcl  9694  zleloe  9700  znnsub  9705  nzadd  9706  zmulcl  9707  zltp1le  9708  zleltp1  9709  nnleltp1  9713  nnltp1le  9714  nnaddm1cl  9715  nn0ltp1le  9716  nn0leltp1  9717  nn0ltlem1  9718  znn0sub  9719  nn0sub  9720  elz2  9725  zapne  9728  zdcle  9730  zdclt  9731  zltlen  9733  nn0lem1lt  9738  nnlem1lt  9739  nnltlem1  9740  fcdmnn0fsuppfi  9743  zdiv  9744  zextle  9747  zextlt  9748  btwnnz  9750  prime  9755  nneo  9759  peano2uz2  9763  peano5uzti  9764  uzind  9767  fzind  9771  fnn0ind  9772  uzneg  9956  uz11  9960  eluzp1m1  9961  eluzp1p1  9963  uzin  9970  indstr  10008  uz2mulcl  10023  qre  10040  qaddcl  10050  qsubcl  10053  qltlen  10055  qlttri2  10056  irradd  10061  elpqb  10066  cnref1o  10067  rpaddcl  10094  rpmulcl  10095  rpdivcl  10096  rexadd  10270  rexsub  10271  xaddcom  10279  xnn0xadd0  10285  xnegdi  10286  elicc2  10356  iccshftr  10412  iccshftl  10414  iccdil  10416  icccntr  10418  fzval2  10430  elfz1eq  10455  peano2fzr  10457  fznlem  10461  fzsplit2  10471  fzsplit3  10474  fzaddel  10481  fzsubel  10482  fzrev2  10508  fzrev3  10510  uzsplit  10515  fzrevral  10528  fzrevral3  10530  fzshftral  10531  elfz2nn0  10535  fznn0sub2  10551  fz0fzdiffz0  10553  elfzmlbp  10555  difelfzle  10557  difelfznle  10558  1fv  10562  elfzouz2  10585  fzo0n  10591  fzouzsplit  10604  fzoun  10606  elfzo0le  10613  fzonmapblen  10615  fzofzim  10616  fzoaddel2  10624  eluzgtdifelfzo  10631  elfzodifsumelfzo  10635  ubmelm1fzo  10660  fzofzp1b  10662  fzosplitprm1  10669  fzostep1  10672  subfzo0  10677  zsupcllemstep  10678  qdclt  10696  qbtwnxr  10708  flqbi2  10746  divfl0  10751  flqzadd  10753  flqmulnn0  10754  addmodidr  10830  modfzo0difsn  10852  frec2uzltd  10860  frec2uzrand  10862  frecfzen2  10884  seqshft2g  10939  seq3split  10945  seqsplitg  10946  seq3caopr2  10950  seqcaopr2g  10951  seqf1oglem2  10977  exp3vallem  10997  expcllem  11007  expcl2lemap  11008  1exp  11025  expge1  11033  expadd  11038  expmul  11041  expsubap  11044  leexp1a  11051  lt2sq  11070  le2sq  11071  sumsqeq0  11075  qsqeqor  11107  bernneq  11118  bernneq2  11119  sq11ap  11165  facdiv  11197  faclbnd  11200  faclbnd3  11202  faclbnd6  11203  facavg  11205  bcrpcl  11212  bccmpl  11213  bcm1n  11228  fiubm  11292  seq3coll  11315  eqwrd  11366  ccatcl  11382  ccatclab  11383  ccatlen  11384  ccat0  11385  ccatval1  11386  ccatval2  11387  elfzelfzccat  11389  ccatvalfn  11390  ccatsymb  11391  ccatval21sw  11394  ccatrn  11398  lswccatn0lsw  11400  ccatalpha  11402  ccatrcl1  11403  swrdfv2  11456  swrdsbslen  11459  swrdspsleq  11460  swrdccat2  11464  pfxclz  11472  ccatpfx  11494  pfxccat1  11495  swrdswrdlem  11497  pfxswrd  11499  pfxccatin12lem4  11519  pfxccatin12lem1  11521  pfxccatin12lem2  11524  pfxccatin12lem3  11525  pfxccat3  11527  swrdccat  11528  pfxccatpfx2  11530  pfxccat3a  11531  swrdccat3blem  11532  swrdccat3b  11533  s2dmg  11583  shftfvalg  11604  shftf  11616  crre  11643  crim  11644  mulreap  11650  readd  11655  resub  11656  remul2  11659  imadd  11663  imsub  11664  immul2  11666  ipcnval  11672  cjsub  11678  cjreim  11690  caucvgre  11768  rexanuz  11775  rexuz3  11777  resqrexlemover  11797  resqrexlemcvg  11806  resqrexlemglsq  11809  sqrtle  11823  sqrtlt  11824  sqrt11ap  11825  sqrt11  11826  absreimsq  11854  absreim  11855  absmul  11856  sqabs  11870  absdiflt  11880  absdifle  11881  abssuble0  11891  abs2difabs  11896  fzomaxdif  11901  caubnd2  11905  rpmaxcl  12011  zmaxcl  12012  nn0maxcl  12013  minmax  12019  mincl  12020  min1inf  12021  min2inf  12022  minabs  12025  minclpr  12026  rpmincl  12027  zmincl  12028  2zinfmin  12033  xrmaxrecl  12045  xrminmax  12055  xrmincl  12056  xrmin1inf  12057  xrmin2inf  12058  xrminrecl  12063  xrminrpcl  12064  iooinsup  12067  climconst2  12081  climuni  12083  2clim  12091  climshft  12094  climshft2  12096  cjcn2  12106  climaddc1  12119  climmulc2  12121  climsubc1  12122  climsubc2  12123  climlec2  12131  summodclem2a  12172  zsumdc  12175  isumclim3  12214  mptfzshft  12233  fsumrev  12234  fisum0diag2  12238  telfsumo2  12258  fsumparts  12261  cvgcmpub  12267  binomlem  12274  binom1p  12276  binom1dif  12278  bcxmas  12280  isumshft  12281  expcnvap0  12293  expcnv  12295  geosergap  12297  geolim  12302  cvgratnnlemrate  12321  mertenslemi1  12326  mertenslem2  12327  mertensabs  12328  prodmodc  12369  zproddc  12370  fprodf1o  12379  fprodeq0  12408  efcj  12464  eftlub  12481  effsumlt  12483  efieq  12526  sinsub  12531  cossub  12532  subsin  12534  sinmul  12535  cosmul  12536  addcos  12537  subcos  12538  dvdssub2  12626  dvdsadd  12627  dvdsaddr  12628  dvdssub  12629  dvdssubr  12630  fzocongeq  12649  odd2np1  12664  opoe  12686  omoe  12687  opeo  12688  omeo  12689  divalgb  12716  ndvdsadd  12722  bitsfi  12748  gcdmndc  12756  gcdabs  12789  dvdsgcd  12813  absmulgcd  12818  gcdmultiple  12821  gcdmultiplez  12822  rpmulgcd  12827  sqgcd  12830  dvdssqlem  12831  dvdssq  12832  nninfctlemfo  12841  nn0seqcvgd  12843  ialgrlemconst  12845  algrf  12847  algrp1  12848  algcvg  12850  algcvga  12853  lcmval  12865  lcmabs  12878  lcmgcd  12880  lcmdvds  12881  lcmgcdnn  12884  coprmgcdb  12890  coprmdvds  12894  coprmdvds2  12895  qredeq  12898  isprm3  12920  nprm  12925  divgcdodd  12946  prmdvdsexp  12951  sqrt2irr  12965  zgcdsq  13005  hashdvds  13027  phiprmpw  13028  crth  13030  phimullem  13031  modprm0  13061  coprimeprodsq  13064  coprimeprodsq2  13065  pythagtriplem2  13073  pythagtriplem19  13089  pcdvdsb  13127  pcneg  13132  pc2dvds  13137  pc11  13138  pcmpt  13150  pcfac  13157  infpnlem1  13166  prmunb  13169  1arithlem4  13173  1arith  13174  gzaddcl  13184  gzmulcl  13185  gzreim  13186  gzsubcl  13187  4sqlem1  13195  4sqlem4a  13198  4sqlem4  13199  4sqlem12  13209  ballotfilemfc0  13289  ballotfilemfcc  13290  setsvalg  13439  setsfun0  13445  restval  13657  mndinvmod  13816  resmhm  13852  resmhm2  13853  mhmco  13855  dfgrp3m  13962  mhmmnd  13977  mulgnngzsum  13988  mulgnn0z  14010  mulgnndir  14012  ghmex  14116  0ghm  14119  resghm  14121  resghm2  14122  ghmco  14125  ghmeql  14128  kerf1ghm  14135  cntzmhm  14172  ablsubsub23  14218  xpsval  14307  dfrhm2  14569  isrhm  14573  rhmfn  14587  rhmval  14588  rhmco  14589  resrhm  14664  rhmeql  14666  rhmima  14667  lmodfopne  14771  lspf  14834  znidom  15100  znrrg  15103  issubassa3  15120  innei  15406  cnovex  15439  txuni2  15499  txbasex  15500  txbas  15501  txtop  15503  txtopon  15505  txss12  15509  txbasval  15510  txcnp  15514  upxp  15515  txcnmpt  15516  uptx  15517  txcn  15518  txrest  15519  txdis  15520  cnmpt21  15534  hmeoco  15559  txhmeo  15562  isxmet2d  15591  blin2  15675  comet  15742  metcn  15757  txmetcn  15762  qtopbasss  15764  qtopbas  15765  remetdval  15790  bl2ioo  15793  blssioo  15796  divcnap  15808  cncfmet  15835  dvaddxxbr  15944  dvcjbr  15951  plyf  15980  ply1termlem  15985  plymullem1  15991  plyaddlem  15992  plymullem  15993  plycolemc  16001  plyreres  16007  dvply1  16008  efle  16019  reapef  16021  sinperlem  16052  sincosq2sgn  16071  sincosq3sgn  16072  sincos6thpi  16086  ioocosf1o  16099  reaplog  16114  relogoprlem  16115  logleb  16122  cxple3  16173  cxpcom  16190  efnthr  16193  birthdaylem2  16243  birthdaylem3  16244  dvdsppwf1o  16300  fsumdvdsmul  16302  1sgmprm  16305  chtublem  16312  mersenne  16314  pcbcctr  16320  bcmono  16321  bposlem1  16328  bposlem2  16329  bposlem3  16330  bposlem5  16332  bposlem6  16333  bposlem7  16334  lgslem3  16343  lgsdir2  16374  lgsdir  16376  lgsdilem2  16377  lgsdi  16378  gausslemma2dlem1a  16399  gausslemma2dlem3  16404  gausslemma2dlem6  16408  lgseisenlem3  16413  lgseisenlem4  16414  lgsquadlem1  16418  lgsquadlem2  16419  lgsquad2  16424  lgsquad3  16425  2lgslem1a1  16427  2lgslem1a  16429  2lgslem1c  16431  2sqlem2  16456  mul2sq  16457  2sqlem7  16462  usgredg2v  16687  ushgredgedg  16689  ushgredgedgloop  16691  uhgrissubgr  16724  vtxedgfi  16752  vtxlpfi  16753  wlkeq  16817  uspgr2wlkeq  16828  clwwlkccatlem  16863  clwwlkccat  16864  clwwlknccat  16886  bj-inex  17155  bj-bdfindis  17195  triap  17301  cvgcmp2nlemabs  17304  trilpolemisumle  17311  inffz  17346