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

Theorem syl2an 277
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 271 . 2  |-  ( (
ph  /\  ch )  ->  th )
51, 4sylan2 274 1  |-  ( (
ph  /\  ta )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem is referenced by:  syl2anr  278  anim12i  325  syl2an2  536  syl2an2r  537  mp3an3an  1249  eqeqan12d  2071  sylan9eq  2108  csbcomg  2901  sylan9ss  2986  ssconb  3104  ineqan12d  3168  dfopg  3575  breqan12d  3807  prelpwi  3978  opexg  3992  copsex2g  4011  ordin  4150  onin  4151  unexg  4206  eusv1  4212  op1stbg  4238  opelvvg  4417  opthprc  4419  opbrop  4447  relop  4514  dmpropg  4821  unixpm  4881  funssres  4970  funtp  4980  fnco  5035  resasplitss  5097  fodmrnu  5142  relrnfvex  5221  fconst2g  5404  fliftel  5461  oveqan12d  5559  ovi3  5665  ovg  5667  f1opw2  5734  off  5752  offres  5790  iunon  5930  nnsucsssuc  6102  nnaword1  6117  ertr  6152  erex  6161  brecop  6227  ecovdi  6248  ecovidi  6249  en2sn  6321  phplem4  6349  ssfiexmid  6367  diffitest  6375  ordiso  6416  finnum  6421  ltsopi  6476  pitric  6477  pitri3or  6478  ltdcpi  6479  mulclpi  6484  addcompig  6485  mulcompig  6487  distrpig  6489  ltexpi  6493  ltapig  6494  ltmpig  6495  dfplpq2  6510  dfmpq2  6511  enqbreq2  6513  enqdc  6517  addcmpblnq  6523  addpipqqslem  6525  mulpipq2  6527  mulpipq  6528  mulpipqqs  6529  addclnq  6531  distrnqg  6543  ltdcnq  6553  ltrnqg  6576  enq0breq  6592  addclnq0  6607  nqnq0a  6610  nqnq0m  6611  nq0m0r  6612  distrnq0  6615  mulcomnq0  6616  genipv  6665  genplt2i  6666  genpelvl  6668  genpelvu  6669  addnqprlemrl  6713  addnqprlemru  6714  addnqprlemfl  6715  addnqprlemfu  6716  addnqpr  6717  mulnqprlemrl  6729  mulnqprlemru  6730  mulnqprlemfl  6731  mulnqprlemfu  6732  mulnqpr  6733  distrlem4prl  6740  distrlem4pru  6741  ltnqpr  6749  recexprlemloc  6787  archrecnq  6819  mulclsr  6897  1idsr  6911  00sr  6912  prsradd  6928  axmulass  7005  axdistr  7006  axcnre  7013  peano5nnnn  7024  mulid1  7082  axltadd  7148  lenlt  7153  cnegexlem3  7251  cnegex  7252  resubcl  7338  subeqrev  7446  muladd  7453  mulsub  7470  mulsub2  7471  ltaddsub2  7506  leaddsub2  7508  leltadd  7516  ltaddpos2  7522  posdif  7524  addge02  7542  mullt0  7549  recexre  7643  recextlem1  7706  recexap  7708  divmuldivap  7763  conjmulap  7780  prodgt02  7894  prodge02  7896  lemul2  7898  lemul2a  7900  ltmulgt12  7906  lemulge12  7908  ltmuldiv2  7916  ltdivmul2  7919  ledivmul2  7921  lemuldiv2  7923  cju  7989  peano5nni  7993  nnaddcl  8010  nnmulcl  8011  nnsub  8028  addltmul  8218  avgle1  8222  avgle2  8223  nnrecl  8237  nn0nnaddcl  8270  zsubcl  8343  zleloe  8349  znnsub  8353  nzadd  8354  zmulcl  8355  zltp1le  8356  zleltp1  8357  nnleltp1  8361  nnltp1le  8362  nnaddm1cl  8363  nn0ltp1le  8364  nn0leltp1  8365  nn0ltlem1  8366  znn0sub  8367  nn0sub  8368  elz2  8370  zapne  8373  zdcle  8375  zdclt  8376  zltlen  8377  nn0lem1lt  8381  nnlem1lt  8382  nnltlem1  8383  zdiv  8386  zextle  8389  zextlt  8390  btwnnz  8392  prime  8396  nneo  8400  peano2uz2  8404  peano5uzti  8405  uzind  8408  fzind  8412  fnn0ind  8413  uzneg  8587  uz11  8591  eluzp1m1  8592  eluzp1p1  8594  uzin  8601  indstr  8632  uz2mulcl  8642  qre  8657  qaddcl  8667  qsubcl  8670  qltlen  8672  qlttri2  8673  irradd  8678  cnref1o  8680  rpaddcl  8704  rpmulcl  8705  rpdivcl  8706  elicc2  8908  iccshftr  8963  iccshftl  8965  iccdil  8967  icccntr  8969  fzval2  8979  elfz1eq  9001  peano2fzr  9003  fznlem  9007  fzsplit2  9016  fzaddel  9024  fzsubel  9025  fzrev2  9049  fzrev3  9051  uzsplit  9056  fzrevral  9069  fzrevral3  9071  fzshftral  9072  elfz2nn0  9075  elfz0addOLD  9082  fznn0sub2  9087  fz0fzdiffz0  9089  elfzmlbp  9092  difelfzle  9094  difelfznle  9095  1fv  9098  elfzouz2  9119  fzouzsplit  9137  elfzo0le  9143  fzonmapblen  9145  fzofzim  9146  fzoaddel2  9151  eluzgtdifelfzo  9155  elfzodifsumelfzo  9159  ubmelm1fzo  9184  fzofzp1b  9186  fzosplitprm1  9192  fzostep1  9195  subfzo0  9199  qbtwnxr  9214  flqbi2  9241  divfl0  9246  flqzadd  9248  flqmulnn0  9249  addmodidr  9323  modfzo0difsn  9345  frec2uzltd  9353  frec2uzrand  9355  frecfzen2  9368  iseqshft2  9396  iseqsplit  9402  iseqcaopr2  9405  expcllem  9431  expcl2lemap  9432  1exp  9449  expge1  9457  expadd  9462  expmul  9465  expsubap  9468  leexp1a  9475  lt2sq  9493  le2sq  9494  sumsqeq0  9498  bernneq  9537  bernneq2  9538  sq11ap  9583  facdiv  9606  faclbnd  9609  faclbnd3  9611  faclbnd6  9612  facavg  9614  bcrpcl  9621  bccmpl  9622  shftfvalg  9647  shftf  9659  crre  9685  crim  9686  mulreap  9692  readd  9697  resub  9698  remul2  9701  imadd  9705  imsub  9706  immul2  9708  ipcnval  9714  cjsub  9720  cjreim  9731  caucvgre  9808  rexanuz  9815  rexuz3  9817  resqrexlemover  9837  resqrexlemcvg  9846  resqrexlemglsq  9849  sqrtle  9863  sqrtlt  9864  sqrt11ap  9865  sqrt11  9866  absreimsq  9894  absreim  9895  absmul  9896  sqabs  9909  absdiflt  9919  absdifle  9920  abssuble0  9930  abs2difabs  9935  fzomaxdif  9940  caubnd2  9944  climconst2  10043  climuni  10045  2clim  10053  climshft  10056  climshft2  10058  cjcn2  10067  climaddc1  10080  climmulc2  10082  climsubc1  10083  climsubc2  10084  climlec2  10092  dvdssub2  10149  dvdsadd  10150  dvdsaddr  10151  dvdssub  10152  dvdssubr  10153  fzocongeq  10170  odd2np1  10184  opoe  10207  omoe  10208  opeo  10209  omeo  10210  divalgb  10237  ndvdsadd  10243  sqrt2irr  10251  nn0seqcvgd  10263  ialgrlemconst  10265  ialgrp1  10268  ialgcvg  10270  ialgcvga  10273  bj-inex  10414  bj-bdfindis  10459
  Copyright terms: Public domain W3C validator