ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  syl2an Unicode version

Theorem syl2an 283
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
StepHypRef Expression
1 syl2an.2 . 2  |-  ( ta 
->  ch )
2 syl2an.1 . . 3  |-  ( ph  ->  ps )
3 syl2an.3 . . 3  |-  ( ( ps  /\  ch )  ->  th )
42, 3sylan 277 . 2  |-  ( (
ph  /\  ch )  ->  th )
51, 4sylan2 280 1  |-  ( (
ph  /\  ta )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem is referenced by:  syl2anr  284  anim12i  331  syl2an2  561  syl2an2r  562  mp3an3an  1279  eqeqan12d  2103  sylan9eq  2140  csbcomg  2952  sylan9ss  3036  ssconb  3131  ineqan12d  3201  dfopg  3615  breqan12d  3852  opexg  4046  copsex2g  4064  ordin  4203  onin  4204  unexg  4259  eusv1  4265  opelvvg  4475  opthprc  4477  opbrop  4505  relop  4574  dmpropg  4890  unixpm  4953  funssres  5042  funinsn  5049  funtp  5053  fnco  5108  resasplitss  5174  fodmrnu  5225  relrnfvex  5307  fconst2g  5494  oveqan12d  5653  ovi3  5763  ovg  5765  f1opw2  5832  off  5850  offres  5888  iunon  6031  nnsucsssuc  6235  nnaword1  6252  ertr  6287  erex  6296  brecop  6362  ecovdi  6383  ecovidi  6384  mapvalg  6395  pmvalg  6396  pmss12g  6412  mapsn  6427  en2sn  6510  xpf1o  6540  xpen  6541  phplem4  6551  ssfilem  6571  diffitest  6583  en1eqsn  6636  sbthlem7  6651  ordiso  6708  updjud  6752  fodjuomnilem0  6781  finnum  6790  pr2nelem  6798  ltsopi  6858  pitric  6859  pitri3or  6860  ltdcpi  6861  mulclpi  6866  addcompig  6867  mulcompig  6869  distrpig  6871  ltexpi  6875  ltapig  6876  ltmpig  6877  dfplpq2  6892  dfmpq2  6893  enqbreq2  6895  enqdc  6899  addcmpblnq  6905  addpipqqslem  6907  mulpipq2  6909  mulpipq  6910  mulpipqqs  6911  addclnq  6913  distrnqg  6925  ltdcnq  6935  ltrnqg  6958  enq0breq  6974  addclnq0  6989  nqnq0a  6992  nqnq0m  6993  nq0m0r  6994  distrnq0  6997  mulcomnq0  6998  genipv  7047  genplt2i  7048  genpelvl  7050  genpelvu  7051  addnqprlemrl  7095  addnqprlemru  7096  addnqprlemfl  7097  addnqprlemfu  7098  addnqpr  7099  mulnqprlemrl  7111  mulnqprlemru  7112  mulnqprlemfl  7113  mulnqprlemfu  7114  mulnqpr  7115  distrlem4prl  7122  distrlem4pru  7123  ltnqpr  7131  recexprlemloc  7169  archrecnq  7201  mulclsr  7279  1idsr  7293  00sr  7294  prsradd  7310  axmulass  7387  axdistr  7388  axcnre  7395  peano5nnnn  7406  mulid1  7464  axltadd  7535  lenlt  7540  cnegexlem3  7638  cnegex  7639  resubcl  7725  subeqrev  7833  muladd  7841  mulsub  7858  mulsub2  7859  ltaddsub2  7894  leaddsub2  7896  leltadd  7904  ltaddpos2  7910  posdif  7912  addge02  7930  mullt0  7937  recexre  8031  recextlem1  8094  recexap  8096  divmuldivap  8153  conjmulap  8170  div2subap  8274  prodgt02  8286  prodge02  8288  lemul2  8290  lemul2a  8292  ltmulgt12  8298  lemulge12  8300  ltmuldiv2  8308  ltdivmul2  8311  ledivmul2  8313  lemuldiv2  8315  negiso  8388  cju  8393  peano5nni  8397  nnaddcl  8414  nnmulcl  8415  nnsub  8432  addltmul  8622  avgle1  8626  avgle2  8627  nnrecl  8641  nn0nnaddcl  8674  zsubcl  8761  zleloe  8767  znnsub  8771  nzadd  8772  zmulcl  8773  zltp1le  8774  zleltp1  8775  nnleltp1  8779  nnltp1le  8780  nnaddm1cl  8781  nn0ltp1le  8782  nn0leltp1  8783  nn0ltlem1  8784  znn0sub  8785  nn0sub  8786  elz2  8788  zapne  8791  zdcle  8793  zdclt  8794  zltlen  8795  nn0lem1lt  8799  nnlem1lt  8800  nnltlem1  8801  zdiv  8804  zextle  8807  zextlt  8808  btwnnz  8810  prime  8815  nneo  8819  peano2uz2  8823  peano5uzti  8824  uzind  8827  fzind  8831  fnn0ind  8832  uzneg  9006  uz11  9010  eluzp1m1  9011  eluzp1p1  9013  uzin  9020  indstr  9050  uz2mulcl  9064  qre  9079  qaddcl  9089  qsubcl  9092  qltlen  9094  qlttri2  9095  irradd  9100  cnref1o  9102  rpaddcl  9126  rpmulcl  9127  rpdivcl  9128  elicc2  9325  iccshftr  9380  iccshftl  9382  iccdil  9384  icccntr  9386  fzval2  9396  elfz1eq  9418  peano2fzr  9420  fznlem  9424  fzsplit2  9433  fzaddel  9441  fzsubel  9442  fzrev2  9466  fzrev3  9468  uzsplit  9473  fzrevral  9486  fzrevral3  9488  fzshftral  9489  elfz2nn0  9493  fznn0sub2  9504  fz0fzdiffz0  9506  elfzmlbp  9508  difelfzle  9510  difelfznle  9511  1fv  9515  elfzouz2  9537  fzouzsplit  9555  elfzo0le  9561  fzonmapblen  9563  fzofzim  9564  fzoaddel2  9569  eluzgtdifelfzo  9573  elfzodifsumelfzo  9577  ubmelm1fzo  9602  fzofzp1b  9604  fzosplitprm1  9610  fzostep1  9613  subfzo0  9618  qbtwnxr  9634  flqbi2  9663  divfl0  9668  flqzadd  9670  flqmulnn0  9671  addmodidr  9745  modfzo0difsn  9767  frec2uzltd  9775  frec2uzrand  9777  frecfzen2  9799  iseqshft2  9863  seq3split  9872  iseqsplit  9873  iseqcaopr2  9876  exp3vallem  9921  expcllem  9931  expcl2lemap  9932  1exp  9949  expge1  9957  expadd  9962  expmul  9965  expsubap  9968  leexp1a  9975  lt2sq  9993  le2sq  9994  sumsqeq0  9998  bernneq  10039  bernneq2  10040  sq11ap  10085  facdiv  10111  faclbnd  10114  faclbnd3  10116  faclbnd6  10117  facavg  10119  bcrpcl  10126  bccmpl  10127  iseqcoll  10212  shftfvalg  10217  shftf  10229  crre  10256  crim  10257  mulreap  10263  readd  10268  resub  10269  remul2  10272  imadd  10276  imsub  10277  immul2  10279  ipcnval  10285  cjsub  10291  cjreim  10302  caucvgre  10379  rexanuz  10386  rexuz3  10388  resqrexlemover  10408  resqrexlemcvg  10417  resqrexlemglsq  10420  sqrtle  10434  sqrtlt  10435  sqrt11ap  10436  sqrt11  10437  absreimsq  10465  absreim  10466  absmul  10467  sqabs  10480  absdiflt  10490  absdifle  10491  abssuble0  10501  abs2difabs  10506  fzomaxdif  10511  caubnd2  10515  zmaxcl  10621  minmax  10625  min1inf  10626  min2inf  10627  climconst2  10643  climuni  10645  2clim  10653  climshft  10656  climshft2  10659  cjcn2  10668  climaddc1  10681  climmulc2  10683  climsubc1  10684  climsubc2  10685  climlec2  10694  isummolem2a  10735  zisum  10738  isumclim3  10780  mptfzshft  10799  fsumrev  10800  fisum0diag2  10804  telfsumo2  10824  fsumparts  10827  cvgcmpub  10832  binomlem  10839  binom1p  10841  binom1dif  10843  bcxmas  10845  isumshft  10846  expcnvap0  10857  expcnv  10859  geosergap  10861  geolim  10866  cvgratnnlemrate  10885  dvdssub2  10931  dvdsadd  10932  dvdsaddr  10933  dvdssub  10934  dvdssubr  10935  fzocongeq  10952  odd2np1  10966  opoe  10988  omoe  10989  opeo  10990  omeo  10991  divalgb  11018  ndvdsadd  11024  zsupcllemstep  11034  gcdabs  11072  dvdsgcd  11094  absmulgcd  11099  gcdmultiple  11102  gcdmultiplez  11103  rpmulgcd  11108  sqgcd  11111  dvdssqlem  11112  dvdssq  11113  nn0seqcvgd  11116  ialgrlemconst  11118  ialgrp1  11121  ialgcvg  11123  ialgcvga  11126  lcmval  11138  lcmabs  11151  lcmgcd  11153  lcmdvds  11154  lcmgcdnn  11157  coprmgcdb  11163  coprmdvds  11167  coprmdvds2  11168  qredeq  11171  isprm3  11193  nprm  11198  divgcdodd  11215  prmdvdsexp  11220  sqrt2irr  11234  zgcdsq  11272  hashdvds  11290  phiprmpw  11291  crth  11293  phimullem  11294  bj-inex  11455  bj-bdfindis  11499  inffz  11574
  Copyright terms: Public domain W3C validator