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  6559  nnsucsssuc  6769  nnaword1  6790  ertr  6826  erex  6835  brecop  6903  ecovdi  6924  ecovidi  6925  mapvalg  6936  pmvalg  6937  pmss12g  6960  mapsn  6976  en2sn  7106  xpf1o  7148  xpen  7149  phplem4  7160  ssfilem  7181  ssfilemd  7183  diffitest  7195  en1eqsn  7270  sbthlem7  7285  fsuppxpfi  7301  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  9696  zleloe  9702  znnsub  9707  nzadd  9708  zmulcl  9709  zltp1le  9710  zleltp1  9711  nnleltp1  9715  nnltp1le  9716  nnaddm1cl  9717  nn0ltp1le  9718  nn0leltp1  9719  nn0ltlem1  9720  znn0sub  9721  nn0sub  9722  elz2  9727  zapne  9730  zdcle  9732  zdclt  9733  zltlen  9735  nn0lem1lt  9740  nnlem1lt  9741  nnltlem1  9742  zdiv  9745  zextle  9748  zextlt  9749  btwnnz  9751  prime  9756  nneo  9760  peano2uz2  9764  peano5uzti  9765  uzind  9768  fzind  9772  fnn0ind  9773  uzneg  9957  uz11  9961  eluzp1m1  9962  eluzp1p1  9964  uzin  9971  indstr  10009  uz2mulcl  10024  qre  10041  qaddcl  10051  qsubcl  10054  qltlen  10056  qlttri2  10057  irradd  10062  elpqb  10067  cnref1o  10068  rpaddcl  10095  rpmulcl  10096  rpdivcl  10097  rexadd  10271  rexsub  10272  xaddcom  10280  xnn0xadd0  10286  xnegdi  10287  elicc2  10357  iccshftr  10413  iccshftl  10415  iccdil  10417  icccntr  10419  fzval2  10431  elfz1eq  10456  peano2fzr  10458  fznlem  10462  fzsplit2  10472  fzsplit3  10475  fzaddel  10482  fzsubel  10483  fzrev2  10509  fzrev3  10511  uzsplit  10516  fzrevral  10529  fzrevral3  10531  fzshftral  10532  elfz2nn0  10536  fznn0sub2  10552  fz0fzdiffz0  10554  elfzmlbp  10556  difelfzle  10558  difelfznle  10559  1fv  10563  elfzouz2  10586  fzo0n  10592  fzouzsplit  10605  fzoun  10607  elfzo0le  10614  fzonmapblen  10616  fzofzim  10617  fzoaddel2  10625  eluzgtdifelfzo  10632  elfzodifsumelfzo  10636  ubmelm1fzo  10661  fzofzp1b  10663  fzosplitprm1  10670  fzostep1  10673  subfzo0  10678  zsupcllemstep  10679  qdclt  10697  qbtwnxr  10709  flqbi2  10747  divfl0  10752  flqzadd  10754  flqmulnn0  10755  addmodidr  10831  modfzo0difsn  10853  frec2uzltd  10861  frec2uzrand  10863  frecfzen2  10885  seqshft2g  10940  seq3split  10946  seqsplitg  10947  seq3caopr2  10951  seqcaopr2g  10952  seqf1oglem2  10978  exp3vallem  10998  expcllem  11008  expcl2lemap  11009  1exp  11026  expge1  11034  expadd  11039  expmul  11042  expsubap  11045  leexp1a  11052  lt2sq  11071  le2sq  11072  sumsqeq0  11076  qsqeqor  11108  bernneq  11119  bernneq2  11120  sq11ap  11166  facdiv  11198  faclbnd  11201  faclbnd3  11203  faclbnd6  11204  facavg  11206  bcrpcl  11213  bccmpl  11214  bcm1n  11229  fiubm  11293  seq3coll  11316  eqwrd  11367  ccatcl  11383  ccatclab  11384  ccatlen  11385  ccat0  11386  ccatval1  11387  ccatval2  11388  elfzelfzccat  11390  ccatvalfn  11391  ccatsymb  11392  ccatval21sw  11395  ccatrn  11399  lswccatn0lsw  11401  ccatalpha  11403  ccatrcl1  11404  swrdfv2  11457  swrdsbslen  11460  swrdspsleq  11461  swrdccat2  11465  pfxclz  11473  ccatpfx  11495  pfxccat1  11496  swrdswrdlem  11498  pfxswrd  11500  pfxccatin12lem4  11520  pfxccatin12lem1  11522  pfxccatin12lem2  11525  pfxccatin12lem3  11526  pfxccat3  11528  swrdccat  11529  pfxccatpfx2  11531  pfxccat3a  11532  swrdccat3blem  11533  swrdccat3b  11534  s2dmg  11584  shftfvalg  11605  shftf  11617  crre  11644  crim  11645  mulreap  11651  readd  11656  resub  11657  remul2  11660  imadd  11664  imsub  11665  immul2  11667  ipcnval  11673  cjsub  11679  cjreim  11691  caucvgre  11769  rexanuz  11776  rexuz3  11778  resqrexlemover  11798  resqrexlemcvg  11807  resqrexlemglsq  11810  sqrtle  11824  sqrtlt  11825  sqrt11ap  11826  sqrt11  11827  absreimsq  11855  absreim  11856  absmul  11857  sqabs  11871  absdiflt  11881  absdifle  11882  abssuble0  11892  abs2difabs  11897  fzomaxdif  11902  caubnd2  11906  rpmaxcl  12012  zmaxcl  12013  nn0maxcl  12014  minmax  12020  mincl  12021  min1inf  12022  min2inf  12023  minabs  12026  minclpr  12027  rpmincl  12028  zmincl  12029  2zinfmin  12034  xrmaxrecl  12046  xrminmax  12056  xrmincl  12057  xrmin1inf  12058  xrmin2inf  12059  xrminrecl  12064  xrminrpcl  12065  iooinsup  12068  climconst2  12082  climuni  12084  2clim  12092  climshft  12095  climshft2  12097  cjcn2  12107  climaddc1  12120  climmulc2  12122  climsubc1  12123  climsubc2  12124  climlec2  12132  summodclem2a  12173  zsumdc  12176  isumclim3  12215  mptfzshft  12234  fsumrev  12235  fisum0diag2  12239  telfsumo2  12259  fsumparts  12262  cvgcmpub  12268  binomlem  12275  binom1p  12277  binom1dif  12279  bcxmas  12281  isumshft  12282  expcnvap0  12294  expcnv  12296  geosergap  12298  geolim  12303  cvgratnnlemrate  12322  mertenslemi1  12327  mertenslem2  12328  mertensabs  12329  prodmodc  12370  zproddc  12371  fprodf1o  12380  fprodeq0  12409  efcj  12465  eftlub  12482  effsumlt  12484  efieq  12527  sinsub  12532  cossub  12533  subsin  12535  sinmul  12536  cosmul  12537  addcos  12538  subcos  12539  dvdssub2  12627  dvdsadd  12628  dvdsaddr  12629  dvdssub  12630  dvdssubr  12631  fzocongeq  12650  odd2np1  12665  opoe  12687  omoe  12688  opeo  12689  omeo  12690  divalgb  12717  ndvdsadd  12723  bitsfi  12749  gcdmndc  12757  gcdabs  12790  dvdsgcd  12814  absmulgcd  12819  gcdmultiple  12822  gcdmultiplez  12823  rpmulgcd  12828  sqgcd  12831  dvdssqlem  12832  dvdssq  12833  nninfctlemfo  12842  nn0seqcvgd  12844  ialgrlemconst  12846  algrf  12848  algrp1  12849  algcvg  12851  algcvga  12854  lcmval  12866  lcmabs  12879  lcmgcd  12881  lcmdvds  12882  lcmgcdnn  12885  coprmgcdb  12891  coprmdvds  12895  coprmdvds2  12896  qredeq  12899  isprm3  12921  nprm  12926  divgcdodd  12947  prmdvdsexp  12952  sqrt2irr  12966  zgcdsq  13006  hashdvds  13028  phiprmpw  13029  crth  13031  phimullem  13032  modprm0  13062  coprimeprodsq  13065  coprimeprodsq2  13066  pythagtriplem2  13074  pythagtriplem19  13090  pcdvdsb  13128  pcneg  13133  pc2dvds  13138  pc11  13139  pcmpt  13151  pcfac  13158  infpnlem1  13167  prmunb  13170  1arithlem4  13174  1arith  13175  gzaddcl  13185  gzmulcl  13186  gzreim  13187  gzsubcl  13188  4sqlem1  13196  4sqlem4a  13199  4sqlem4  13200  4sqlem12  13210  ballotfilemfc0  13290  ballotfilemfcc  13291  setsvalg  13440  setsfun0  13446  restval  13658  mndinvmod  13817  resmhm  13853  resmhm2  13854  mhmco  13856  dfgrp3m  13963  mhmmnd  13978  mulgnngzsum  13989  mulgnn0z  14011  mulgnndir  14013  ghmex  14117  0ghm  14120  resghm  14122  resghm2  14123  ghmco  14126  ghmeql  14129  kerf1ghm  14136  cntzmhm  14173  ablsubsub23  14219  xpsval  14308  dfrhm2  14570  isrhm  14574  rhmfn  14588  rhmval  14589  rhmco  14590  resrhm  14665  rhmeql  14667  rhmima  14668  lmodfopne  14772  lspf  14835  znidom  15101  znrrg  15104  issubassa3  15121  innei  15389  cnovex  15422  txuni2  15482  txbasex  15483  txbas  15484  txtop  15486  txtopon  15488  txss12  15492  txbasval  15493  txcnp  15497  upxp  15498  txcnmpt  15499  uptx  15500  txcn  15501  txrest  15502  txdis  15503  cnmpt21  15517  hmeoco  15542  txhmeo  15545  isxmet2d  15574  blin2  15658  comet  15725  metcn  15740  txmetcn  15745  qtopbasss  15747  qtopbas  15748  remetdval  15773  bl2ioo  15776  blssioo  15779  divcnap  15791  cncfmet  15818  dvaddxxbr  15927  dvcjbr  15934  plyf  15963  ply1termlem  15968  plymullem1  15974  plyaddlem  15975  plymullem  15976  plycolemc  15984  plyreres  15990  dvply1  15991  efle  16002  reapef  16004  sinperlem  16035  sincosq2sgn  16054  sincosq3sgn  16055  sincos6thpi  16069  ioocosf1o  16082  reaplog  16097  relogoprlem  16098  logleb  16105  cxple3  16156  cxpcom  16173  efnthr  16176  birthdaylem2  16226  birthdaylem3  16227  dvdsppwf1o  16283  fsumdvdsmul  16285  1sgmprm  16288  chtublem  16295  mersenne  16297  pcbcctr  16303  bcmono  16304  bposlem1  16311  bposlem2  16312  bposlem3  16313  bposlem5  16315  bposlem6  16316  bposlem7  16317  lgslem3  16326  lgsdir2  16357  lgsdir  16359  lgsdilem2  16360  lgsdi  16361  gausslemma2dlem1a  16382  gausslemma2dlem3  16387  gausslemma2dlem6  16391  lgseisenlem3  16396  lgseisenlem4  16397  lgsquadlem1  16401  lgsquadlem2  16402  lgsquad2  16407  lgsquad3  16408  2lgslem1a1  16410  2lgslem1a  16412  2lgslem1c  16414  2sqlem2  16439  mul2sq  16440  2sqlem7  16445  usgredg2v  16670  ushgredgedg  16672  ushgredgedgloop  16674  uhgrissubgr  16707  vtxedgfi  16735  vtxlpfi  16736  wlkeq  16800  uspgr2wlkeq  16811  clwwlkccatlem  16846  clwwlkccat  16847  clwwlknccat  16869  bj-inex  17138  bj-bdfindis  17178  triap  17284  cvgcmp2nlemabs  17287  trilpolemisumle  17294  inffz  17329