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  594  syl2an2r  595  mp3an3an  1343  eqeqan12d  2193  sylan9eq  2230  csbcomg  3082  sylan9ss  3170  ssconb  3270  ineqan12d  3340  dfopg  3778  breqan12d  4021  opexg  4230  copsex2g  4248  ordin  4387  onin  4388  unexg  4445  eusv1  4454  opelvvg  4677  opthprc  4679  opbrop  4707  relop  4779  dmpropg  5103  unixpm  5166  funssres  5260  funinsn  5267  funtp  5271  fnco  5326  resasplitss  5397  fodmrnu  5448  relrnfvex  5535  fconst2g  5733  oveqan12d  5896  ovi3  6013  ovg  6015  f1opw2  6079  off  6097  offres  6138  iunon  6287  nnsucsssuc  6495  nnaword1  6516  ertr  6552  erex  6561  brecop  6627  ecovdi  6648  ecovidi  6649  mapvalg  6660  pmvalg  6661  pmss12g  6677  mapsn  6692  en2sn  6815  xpf1o  6846  xpen  6847  phplem4  6857  ssfilem  6877  diffitest  6889  en1eqsn  6949  sbthlem7  6964  ordiso  7037  updjud  7083  fodju0  7147  finnum  7184  pr2nelem  7192  djucomen  7217  exmidontriimlem1  7222  2onetap  7256  ltsopi  7321  pitric  7322  pitri3or  7323  ltdcpi  7324  mulclpi  7329  addcompig  7330  mulcompig  7332  distrpig  7334  ltexpi  7338  ltapig  7339  ltmpig  7340  dfplpq2  7355  dfmpq2  7356  enqbreq2  7358  enqdc  7362  addcmpblnq  7368  addpipqqslem  7370  mulpipq2  7372  mulpipq  7373  mulpipqqs  7374  addclnq  7376  distrnqg  7388  ltdcnq  7398  ltrnqg  7421  enq0breq  7437  addclnq0  7452  nqnq0a  7455  nqnq0m  7456  nq0m0r  7457  distrnq0  7460  mulcomnq0  7461  genipv  7510  genplt2i  7511  genpelvl  7513  genpelvu  7514  addnqprlemrl  7558  addnqprlemru  7559  addnqprlemfl  7560  addnqprlemfu  7561  addnqpr  7562  mulnqprlemrl  7574  mulnqprlemru  7575  mulnqprlemfl  7576  mulnqprlemfu  7577  mulnqpr  7578  distrlem4prl  7585  distrlem4pru  7586  ltnqpr  7594  recexprlemloc  7632  archrecnq  7664  mulclsr  7755  1idsr  7769  00sr  7770  prsradd  7787  axmulass  7874  axdistr  7875  axcnre  7882  peano5nnnn  7893  mulrid  7956  axltadd  8029  lenlt  8035  cnegexlem3  8136  cnegex  8137  resubcl  8223  subeqrev  8335  muladd  8343  mulsub  8360  mulsub2  8361  ltaddsub2  8396  leaddsub2  8398  leltadd  8406  ltaddpos2  8412  posdif  8414  addge02  8432  mullt0  8439  recexre  8537  recextlem1  8610  recexap  8612  divmuldivap  8671  conjmulap  8688  div2subap  8796  prodgt02  8812  prodge02  8814  lemul2  8816  lemul2a  8818  ltmulgt12  8824  lemulge12  8826  ltmuldiv2  8834  ltdivmul2  8837  ledivmul2  8839  lemuldiv2  8841  negiso  8914  cju  8920  peano5nni  8924  nnaddcl  8941  nnmulcl  8942  nnsub  8960  addltmul  9157  avgle1  9161  avgle2  9162  nnrecl  9176  nn0nnaddcl  9209  zsubcl  9296  zleloe  9302  znnsub  9306  nzadd  9307  zmulcl  9308  zltp1le  9309  zleltp1  9310  nnleltp1  9314  nnltp1le  9315  nnaddm1cl  9316  nn0ltp1le  9317  nn0leltp1  9318  nn0ltlem1  9319  znn0sub  9320  nn0sub  9321  elz2  9326  zapne  9329  zdcle  9331  zdclt  9332  zltlen  9333  nn0lem1lt  9338  nnlem1lt  9339  nnltlem1  9340  zdiv  9343  zextle  9346  zextlt  9347  btwnnz  9349  prime  9354  nneo  9358  peano2uz2  9362  peano5uzti  9363  uzind  9366  fzind  9370  fnn0ind  9371  uzneg  9548  uz11  9552  eluzp1m1  9553  eluzp1p1  9555  uzin  9562  indstr  9595  uz2mulcl  9610  qre  9627  qaddcl  9637  qsubcl  9640  qltlen  9642  qlttri2  9643  irradd  9648  elpqb  9651  cnref1o  9652  rpaddcl  9679  rpmulcl  9680  rpdivcl  9681  rexadd  9854  rexsub  9855  xaddcom  9863  xnn0xadd0  9869  xnegdi  9870  elicc2  9940  iccshftr  9996  iccshftl  9998  iccdil  10000  icccntr  10002  fzval2  10013  elfz1eq  10037  peano2fzr  10039  fznlem  10043  fzsplit2  10052  fzaddel  10061  fzsubel  10062  fzrev2  10087  fzrev3  10089  uzsplit  10094  fzrevral  10107  fzrevral3  10109  fzshftral  10110  elfz2nn0  10114  fznn0sub2  10130  fz0fzdiffz0  10132  elfzmlbp  10134  difelfzle  10136  difelfznle  10137  1fv  10141  elfzouz2  10163  fzouzsplit  10181  elfzo0le  10187  fzonmapblen  10189  fzofzim  10190  fzoaddel2  10195  eluzgtdifelfzo  10199  elfzodifsumelfzo  10203  ubmelm1fzo  10228  fzofzp1b  10230  fzosplitprm1  10236  fzostep1  10239  subfzo0  10244  qbtwnxr  10260  flqbi2  10293  divfl0  10298  flqzadd  10300  flqmulnn0  10301  addmodidr  10375  modfzo0difsn  10397  frec2uzltd  10405  frec2uzrand  10407  frecfzen2  10429  seq3split  10481  seq3caopr2  10484  exp3vallem  10523  expcllem  10533  expcl2lemap  10534  1exp  10551  expge1  10559  expadd  10564  expmul  10567  expsubap  10570  leexp1a  10577  lt2sq  10596  le2sq  10597  sumsqeq0  10601  qsqeqor  10633  bernneq  10643  bernneq2  10644  sq11ap  10690  facdiv  10720  faclbnd  10723  faclbnd3  10725  faclbnd6  10726  facavg  10728  bcrpcl  10735  bccmpl  10736  fiubm  10810  seq3coll  10824  shftfvalg  10829  shftf  10841  crre  10868  crim  10869  mulreap  10875  readd  10880  resub  10881  remul2  10884  imadd  10888  imsub  10889  immul2  10891  ipcnval  10897  cjsub  10903  cjreim  10914  caucvgre  10992  rexanuz  10999  rexuz3  11001  resqrexlemover  11021  resqrexlemcvg  11030  resqrexlemglsq  11033  sqrtle  11047  sqrtlt  11048  sqrt11ap  11049  sqrt11  11050  absreimsq  11078  absreim  11079  absmul  11080  sqabs  11093  absdiflt  11103  absdifle  11104  abssuble0  11114  abs2difabs  11119  fzomaxdif  11124  caubnd2  11128  rpmaxcl  11234  zmaxcl  11235  minmax  11240  mincl  11241  min1inf  11242  min2inf  11243  minabs  11246  minclpr  11247  rpmincl  11248  2zinfmin  11253  xrmaxrecl  11265  xrminmax  11275  xrmincl  11276  xrmin1inf  11277  xrmin2inf  11278  xrminrecl  11283  xrminrpcl  11284  iooinsup  11287  climconst2  11301  climuni  11303  2clim  11311  climshft  11314  climshft2  11316  cjcn2  11326  climaddc1  11339  climmulc2  11341  climsubc1  11342  climsubc2  11343  climlec2  11351  summodclem2a  11391  zsumdc  11394  isumclim3  11433  mptfzshft  11452  fsumrev  11453  fisum0diag2  11457  telfsumo2  11477  fsumparts  11480  cvgcmpub  11486  binomlem  11493  binom1p  11495  binom1dif  11497  bcxmas  11499  isumshft  11500  expcnvap0  11512  expcnv  11514  geosergap  11516  geolim  11521  cvgratnnlemrate  11540  mertenslemi1  11545  mertenslem2  11546  mertensabs  11547  prodmodc  11588  zproddc  11589  fprodf1o  11598  fprodeq0  11627  efcj  11683  eftlub  11700  effsumlt  11702  efieq  11745  sinsub  11750  cossub  11751  subsin  11753  sinmul  11754  cosmul  11755  addcos  11756  subcos  11757  dvdssub2  11844  dvdsadd  11845  dvdsaddr  11846  dvdssub  11847  dvdssubr  11848  fzocongeq  11866  odd2np1  11880  opoe  11902  omoe  11903  opeo  11904  omeo  11905  divalgb  11932  ndvdsadd  11938  zsupcllemstep  11948  gcdabs  11991  dvdsgcd  12015  absmulgcd  12020  gcdmultiple  12023  gcdmultiplez  12024  rpmulgcd  12029  sqgcd  12032  dvdssqlem  12033  dvdssq  12034  nn0seqcvgd  12043  ialgrlemconst  12045  algrf  12047  algrp1  12048  algcvg  12050  algcvga  12053  lcmval  12065  lcmabs  12078  lcmgcd  12080  lcmdvds  12081  lcmgcdnn  12084  coprmgcdb  12090  coprmdvds  12094  coprmdvds2  12095  qredeq  12098  isprm3  12120  nprm  12125  divgcdodd  12145  prmdvdsexp  12150  sqrt2irr  12164  zgcdsq  12203  hashdvds  12223  phiprmpw  12224  crth  12226  phimullem  12227  modprm0  12256  coprimeprodsq  12259  coprimeprodsq2  12260  pythagtriplem2  12268  pythagtriplem19  12284  pcdvdsb  12321  pcneg  12326  pc2dvds  12331  pc11  12332  pcmpt  12343  pcfac  12350  infpnlem1  12359  prmunb  12362  1arithlem4  12366  1arith  12367  gzaddcl  12377  gzmulcl  12378  gzreim  12379  gzsubcl  12380  4sqlem1  12388  4sqlem4a  12391  4sqlem4  12392  setsvalg  12494  setsfun0  12500  restval  12699  xpsval  12776  mndinvmod  12851  mhmco  12879  dfgrp3m  12974  mhmmnd  12985  mulgnn0z  13015  mulgnndir  13017  ablsubsub23  13133  lmodfopne  13421  lspf  13481  innei  13748  cnovex  13781  txuni2  13841  txbasex  13842  txbas  13843  txtop  13845  txtopon  13847  txss12  13851  txbasval  13852  txcnp  13856  upxp  13857  txcnmpt  13858  uptx  13859  txcn  13860  txrest  13861  txdis  13862  cnmpt21  13876  hmeoco  13901  txhmeo  13904  isxmet2d  13933  blin2  14017  comet  14084  metcn  14099  txmetcn  14104  qtopbasss  14106  qtopbas  14107  remetdval  14124  bl2ioo  14127  blssioo  14130  divcnap  14140  cncfmet  14164  dvaddxxbr  14250  dvcjbr  14257  efle  14282  reapef  14284  sinperlem  14314  sincosq2sgn  14333  sincosq3sgn  14334  sincos6thpi  14348  ioocosf1o  14360  relogoprlem  14374  logleb  14381  cxple3  14426  cxpcom  14442  lgslem3  14488  lgsdir2  14519  lgsdir  14521  lgsdilem2  14522  lgsdi  14523  2sqlem2  14547  mul2sq  14548  2sqlem7  14553  bj-inex  14744  bj-bdfindis  14784  triap  14862  cvgcmp2nlemabs  14865  trilpolemisumle  14871  inffz  14905