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  3080  sylan9ss  3168  ssconb  3268  ineqan12d  3338  dfopg  3774  breqan12d  4016  opexg  4225  copsex2g  4243  ordin  4382  onin  4383  unexg  4440  eusv1  4449  opelvvg  4672  opthprc  4674  opbrop  4702  relop  4773  dmpropg  5097  unixpm  5160  funssres  5254  funinsn  5261  funtp  5265  fnco  5320  resasplitss  5391  fodmrnu  5442  relrnfvex  5529  fconst2g  5727  oveqan12d  5888  ovi3  6005  ovg  6007  f1opw2  6071  off  6089  offres  6130  iunon  6279  nnsucsssuc  6487  nnaword1  6508  ertr  6544  erex  6553  brecop  6619  ecovdi  6640  ecovidi  6641  mapvalg  6652  pmvalg  6653  pmss12g  6669  mapsn  6684  en2sn  6807  xpf1o  6838  xpen  6839  phplem4  6849  ssfilem  6869  diffitest  6881  en1eqsn  6941  sbthlem7  6956  ordiso  7029  updjud  7075  fodju0  7139  finnum  7176  pr2nelem  7184  djucomen  7209  exmidontriimlem1  7214  2onetap  7245  ltsopi  7310  pitric  7311  pitri3or  7312  ltdcpi  7313  mulclpi  7318  addcompig  7319  mulcompig  7321  distrpig  7323  ltexpi  7327  ltapig  7328  ltmpig  7329  dfplpq2  7344  dfmpq2  7345  enqbreq2  7347  enqdc  7351  addcmpblnq  7357  addpipqqslem  7359  mulpipq2  7361  mulpipq  7362  mulpipqqs  7363  addclnq  7365  distrnqg  7377  ltdcnq  7387  ltrnqg  7410  enq0breq  7426  addclnq0  7441  nqnq0a  7444  nqnq0m  7445  nq0m0r  7446  distrnq0  7449  mulcomnq0  7450  genipv  7499  genplt2i  7500  genpelvl  7502  genpelvu  7503  addnqprlemrl  7547  addnqprlemru  7548  addnqprlemfl  7549  addnqprlemfu  7550  addnqpr  7551  mulnqprlemrl  7563  mulnqprlemru  7564  mulnqprlemfl  7565  mulnqprlemfu  7566  mulnqpr  7567  distrlem4prl  7574  distrlem4pru  7575  ltnqpr  7583  recexprlemloc  7621  archrecnq  7653  mulclsr  7744  1idsr  7758  00sr  7759  prsradd  7776  axmulass  7863  axdistr  7864  axcnre  7871  peano5nnnn  7882  mulid1  7945  axltadd  8017  lenlt  8023  cnegexlem3  8124  cnegex  8125  resubcl  8211  subeqrev  8323  muladd  8331  mulsub  8348  mulsub2  8349  ltaddsub2  8384  leaddsub2  8386  leltadd  8394  ltaddpos2  8400  posdif  8402  addge02  8420  mullt0  8427  recexre  8525  recextlem1  8597  recexap  8599  divmuldivap  8658  conjmulap  8675  div2subap  8783  prodgt02  8799  prodge02  8801  lemul2  8803  lemul2a  8805  ltmulgt12  8811  lemulge12  8813  ltmuldiv2  8821  ltdivmul2  8824  ledivmul2  8826  lemuldiv2  8828  negiso  8901  cju  8907  peano5nni  8911  nnaddcl  8928  nnmulcl  8929  nnsub  8947  addltmul  9144  avgle1  9148  avgle2  9149  nnrecl  9163  nn0nnaddcl  9196  zsubcl  9283  zleloe  9289  znnsub  9293  nzadd  9294  zmulcl  9295  zltp1le  9296  zleltp1  9297  nnleltp1  9301  nnltp1le  9302  nnaddm1cl  9303  nn0ltp1le  9304  nn0leltp1  9305  nn0ltlem1  9306  znn0sub  9307  nn0sub  9308  elz2  9313  zapne  9316  zdcle  9318  zdclt  9319  zltlen  9320  nn0lem1lt  9325  nnlem1lt  9326  nnltlem1  9327  zdiv  9330  zextle  9333  zextlt  9334  btwnnz  9336  prime  9341  nneo  9345  peano2uz2  9349  peano5uzti  9350  uzind  9353  fzind  9357  fnn0ind  9358  uzneg  9535  uz11  9539  eluzp1m1  9540  eluzp1p1  9542  uzin  9549  indstr  9582  uz2mulcl  9597  qre  9614  qaddcl  9624  qsubcl  9627  qltlen  9629  qlttri2  9630  irradd  9635  elpqb  9638  cnref1o  9639  rpaddcl  9664  rpmulcl  9665  rpdivcl  9666  rexadd  9839  rexsub  9840  xaddcom  9848  xnn0xadd0  9854  xnegdi  9855  elicc2  9925  iccshftr  9981  iccshftl  9983  iccdil  9985  icccntr  9987  fzval2  9998  elfz1eq  10021  peano2fzr  10023  fznlem  10027  fzsplit2  10036  fzaddel  10045  fzsubel  10046  fzrev2  10071  fzrev3  10073  uzsplit  10078  fzrevral  10091  fzrevral3  10093  fzshftral  10094  elfz2nn0  10098  fznn0sub2  10114  fz0fzdiffz0  10116  elfzmlbp  10118  difelfzle  10120  difelfznle  10121  1fv  10125  elfzouz2  10147  fzouzsplit  10165  elfzo0le  10171  fzonmapblen  10173  fzofzim  10174  fzoaddel2  10179  eluzgtdifelfzo  10183  elfzodifsumelfzo  10187  ubmelm1fzo  10212  fzofzp1b  10214  fzosplitprm1  10220  fzostep1  10223  subfzo0  10228  qbtwnxr  10244  flqbi2  10277  divfl0  10282  flqzadd  10284  flqmulnn0  10285  addmodidr  10359  modfzo0difsn  10381  frec2uzltd  10389  frec2uzrand  10391  frecfzen2  10413  seq3split  10465  seq3caopr2  10468  exp3vallem  10507  expcllem  10517  expcl2lemap  10518  1exp  10535  expge1  10543  expadd  10548  expmul  10551  expsubap  10554  leexp1a  10561  lt2sq  10579  le2sq  10580  sumsqeq0  10584  qsqeqor  10616  bernneq  10626  bernneq2  10627  sq11ap  10673  facdiv  10702  faclbnd  10705  faclbnd3  10707  faclbnd6  10708  facavg  10710  bcrpcl  10717  bccmpl  10718  fiubm  10792  seq3coll  10806  shftfvalg  10811  shftf  10823  crre  10850  crim  10851  mulreap  10857  readd  10862  resub  10863  remul2  10866  imadd  10870  imsub  10871  immul2  10873  ipcnval  10879  cjsub  10885  cjreim  10896  caucvgre  10974  rexanuz  10981  rexuz3  10983  resqrexlemover  11003  resqrexlemcvg  11012  resqrexlemglsq  11015  sqrtle  11029  sqrtlt  11030  sqrt11ap  11031  sqrt11  11032  absreimsq  11060  absreim  11061  absmul  11062  sqabs  11075  absdiflt  11085  absdifle  11086  abssuble0  11096  abs2difabs  11101  fzomaxdif  11106  caubnd2  11110  rpmaxcl  11216  zmaxcl  11217  minmax  11222  mincl  11223  min1inf  11224  min2inf  11225  minabs  11228  minclpr  11229  rpmincl  11230  2zinfmin  11235  xrmaxrecl  11247  xrminmax  11257  xrmincl  11258  xrmin1inf  11259  xrmin2inf  11260  xrminrecl  11265  xrminrpcl  11266  iooinsup  11269  climconst2  11283  climuni  11285  2clim  11293  climshft  11296  climshft2  11298  cjcn2  11308  climaddc1  11321  climmulc2  11323  climsubc1  11324  climsubc2  11325  climlec2  11333  summodclem2a  11373  zsumdc  11376  isumclim3  11415  mptfzshft  11434  fsumrev  11435  fisum0diag2  11439  telfsumo2  11459  fsumparts  11462  cvgcmpub  11468  binomlem  11475  binom1p  11477  binom1dif  11479  bcxmas  11481  isumshft  11482  expcnvap0  11494  expcnv  11496  geosergap  11498  geolim  11503  cvgratnnlemrate  11522  mertenslemi1  11527  mertenslem2  11528  mertensabs  11529  prodmodc  11570  zproddc  11571  fprodf1o  11580  fprodeq0  11609  efcj  11665  eftlub  11682  effsumlt  11684  efieq  11727  sinsub  11732  cossub  11733  subsin  11735  sinmul  11736  cosmul  11737  addcos  11738  subcos  11739  dvdssub2  11826  dvdsadd  11827  dvdsaddr  11828  dvdssub  11829  dvdssubr  11830  fzocongeq  11847  odd2np1  11861  opoe  11883  omoe  11884  opeo  11885  omeo  11886  divalgb  11913  ndvdsadd  11919  zsupcllemstep  11929  gcdabs  11972  dvdsgcd  11996  absmulgcd  12001  gcdmultiple  12004  gcdmultiplez  12005  rpmulgcd  12010  sqgcd  12013  dvdssqlem  12014  dvdssq  12015  nn0seqcvgd  12024  ialgrlemconst  12026  algrf  12028  algrp1  12029  algcvg  12031  algcvga  12034  lcmval  12046  lcmabs  12059  lcmgcd  12061  lcmdvds  12062  lcmgcdnn  12065  coprmgcdb  12071  coprmdvds  12075  coprmdvds2  12076  qredeq  12079  isprm3  12101  nprm  12106  divgcdodd  12126  prmdvdsexp  12131  sqrt2irr  12145  zgcdsq  12184  hashdvds  12204  phiprmpw  12205  crth  12207  phimullem  12208  modprm0  12237  coprimeprodsq  12240  coprimeprodsq2  12241  pythagtriplem2  12249  pythagtriplem19  12265  pcdvdsb  12302  pcneg  12307  pc2dvds  12312  pc11  12313  pcmpt  12324  pcfac  12331  infpnlem1  12340  prmunb  12343  1arithlem4  12347  1arith  12348  gzaddcl  12358  gzmulcl  12359  gzreim  12360  gzsubcl  12361  4sqlem1  12369  4sqlem4a  12372  4sqlem4  12373  setsvalg  12475  setsfun0  12481  restval  12642  mndinvmod  12736  mhmco  12764  dfgrp3m  12858  mhmmnd  12869  mulgnn0z  12898  mulgnndir  12900  ablsubsub23  12955  innei  13330  cnovex  13363  txuni2  13423  txbasex  13424  txbas  13425  txtop  13427  txtopon  13429  txss12  13433  txbasval  13434  txcnp  13438  upxp  13439  txcnmpt  13440  uptx  13441  txcn  13442  txrest  13443  txdis  13444  cnmpt21  13458  hmeoco  13483  txhmeo  13486  isxmet2d  13515  blin2  13599  comet  13666  metcn  13681  txmetcn  13686  qtopbasss  13688  qtopbas  13689  remetdval  13706  bl2ioo  13709  blssioo  13712  divcnap  13722  cncfmet  13746  dvaddxxbr  13832  dvcjbr  13839  efle  13864  reapef  13866  sinperlem  13896  sincosq2sgn  13915  sincosq3sgn  13916  sincos6thpi  13930  ioocosf1o  13942  relogoprlem  13956  logleb  13963  cxple3  14008  cxpcom  14024  lgslem3  14070  lgsdir2  14101  lgsdir  14103  lgsdilem2  14104  lgsdi  14105  2sqlem2  14118  mul2sq  14119  2sqlem7  14124  bj-inex  14315  bj-bdfindis  14355  triap  14433  cvgcmp2nlemabs  14436  trilpolemisumle  14442  inffz  14473