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

Theorem syl2an 287
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 281 . 2  |-  ( (
ph  /\  ch )  ->  th )
51, 4sylan2 284 1  |-  ( (
ph  /\  ta )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem is referenced by:  syl2anr  288  anim12i  336  syl2an2  584  syl2an2r  585  mp3an3an  1332  eqeqan12d  2180  sylan9eq  2217  csbcomg  3066  sylan9ss  3153  ssconb  3253  ineqan12d  3323  dfopg  3753  breqan12d  3995  opexg  4203  copsex2g  4221  ordin  4360  onin  4361  unexg  4418  eusv1  4427  opelvvg  4650  opthprc  4652  opbrop  4680  relop  4751  dmpropg  5073  unixpm  5136  funssres  5227  funinsn  5234  funtp  5238  fnco  5293  resasplitss  5364  fodmrnu  5415  relrnfvex  5501  fconst2g  5697  oveqan12d  5858  ovi3  5972  ovg  5974  f1opw2  6041  off  6059  offres  6098  iunon  6246  nnsucsssuc  6454  nnaword1  6475  ertr  6510  erex  6519  brecop  6585  ecovdi  6606  ecovidi  6607  mapvalg  6618  pmvalg  6619  pmss12g  6635  mapsn  6650  en2sn  6773  xpf1o  6804  xpen  6805  phplem4  6815  ssfilem  6835  diffitest  6847  en1eqsn  6907  sbthlem7  6922  ordiso  6995  updjud  7041  fodju0  7105  finnum  7133  pr2nelem  7141  djucomen  7166  exmidontriimlem1  7171  ltsopi  7255  pitric  7256  pitri3or  7257  ltdcpi  7258  mulclpi  7263  addcompig  7264  mulcompig  7266  distrpig  7268  ltexpi  7272  ltapig  7273  ltmpig  7274  dfplpq2  7289  dfmpq2  7290  enqbreq2  7292  enqdc  7296  addcmpblnq  7302  addpipqqslem  7304  mulpipq2  7306  mulpipq  7307  mulpipqqs  7308  addclnq  7310  distrnqg  7322  ltdcnq  7332  ltrnqg  7355  enq0breq  7371  addclnq0  7386  nqnq0a  7389  nqnq0m  7390  nq0m0r  7391  distrnq0  7394  mulcomnq0  7395  genipv  7444  genplt2i  7445  genpelvl  7447  genpelvu  7448  addnqprlemrl  7492  addnqprlemru  7493  addnqprlemfl  7494  addnqprlemfu  7495  addnqpr  7496  mulnqprlemrl  7508  mulnqprlemru  7509  mulnqprlemfl  7510  mulnqprlemfu  7511  mulnqpr  7512  distrlem4prl  7519  distrlem4pru  7520  ltnqpr  7528  recexprlemloc  7566  archrecnq  7598  mulclsr  7689  1idsr  7703  00sr  7704  prsradd  7721  axmulass  7808  axdistr  7809  axcnre  7816  peano5nnnn  7827  mulid1  7890  axltadd  7962  lenlt  7968  cnegexlem3  8069  cnegex  8070  resubcl  8156  subeqrev  8268  muladd  8276  mulsub  8293  mulsub2  8294  ltaddsub2  8329  leaddsub2  8331  leltadd  8339  ltaddpos2  8345  posdif  8347  addge02  8365  mullt0  8372  recexre  8470  recextlem1  8542  recexap  8544  divmuldivap  8602  conjmulap  8619  div2subap  8727  prodgt02  8742  prodge02  8744  lemul2  8746  lemul2a  8748  ltmulgt12  8754  lemulge12  8756  ltmuldiv2  8764  ltdivmul2  8767  ledivmul2  8769  lemuldiv2  8771  negiso  8844  cju  8850  peano5nni  8854  nnaddcl  8871  nnmulcl  8872  nnsub  8890  addltmul  9087  avgle1  9091  avgle2  9092  nnrecl  9106  nn0nnaddcl  9139  zsubcl  9226  zleloe  9232  znnsub  9236  nzadd  9237  zmulcl  9238  zltp1le  9239  zleltp1  9240  nnleltp1  9244  nnltp1le  9245  nnaddm1cl  9246  nn0ltp1le  9247  nn0leltp1  9248  nn0ltlem1  9249  znn0sub  9250  nn0sub  9251  elz2  9256  zapne  9259  zdcle  9261  zdclt  9262  zltlen  9263  nn0lem1lt  9268  nnlem1lt  9269  nnltlem1  9270  zdiv  9273  zextle  9276  zextlt  9277  btwnnz  9279  prime  9284  nneo  9288  peano2uz2  9292  peano5uzti  9293  uzind  9296  fzind  9300  fnn0ind  9301  uzneg  9478  uz11  9482  eluzp1m1  9483  eluzp1p1  9485  uzin  9492  indstr  9525  uz2mulcl  9540  qre  9557  qaddcl  9567  qsubcl  9570  qltlen  9572  qlttri2  9573  irradd  9578  elpqb  9581  cnref1o  9582  rpaddcl  9607  rpmulcl  9608  rpdivcl  9609  rexadd  9782  rexsub  9783  xaddcom  9791  xnn0xadd0  9797  xnegdi  9798  elicc2  9868  iccshftr  9924  iccshftl  9926  iccdil  9928  icccntr  9930  fzval2  9941  elfz1eq  9964  peano2fzr  9966  fznlem  9970  fzsplit2  9979  fzaddel  9988  fzsubel  9989  fzrev2  10014  fzrev3  10016  uzsplit  10021  fzrevral  10034  fzrevral3  10036  fzshftral  10037  elfz2nn0  10041  fznn0sub2  10057  fz0fzdiffz0  10059  elfzmlbp  10061  difelfzle  10063  difelfznle  10064  1fv  10068  elfzouz2  10090  fzouzsplit  10108  elfzo0le  10114  fzonmapblen  10116  fzofzim  10117  fzoaddel2  10122  eluzgtdifelfzo  10126  elfzodifsumelfzo  10130  ubmelm1fzo  10155  fzofzp1b  10157  fzosplitprm1  10163  fzostep1  10166  subfzo0  10171  qbtwnxr  10187  flqbi2  10220  divfl0  10225  flqzadd  10227  flqmulnn0  10228  addmodidr  10302  modfzo0difsn  10324  frec2uzltd  10332  frec2uzrand  10334  frecfzen2  10356  seq3split  10408  seq3caopr2  10411  exp3vallem  10450  expcllem  10460  expcl2lemap  10461  1exp  10478  expge1  10486  expadd  10491  expmul  10494  expsubap  10497  leexp1a  10504  lt2sq  10522  le2sq  10523  sumsqeq0  10527  qsqeqor  10559  bernneq  10569  bernneq2  10570  sq11ap  10616  facdiv  10645  faclbnd  10648  faclbnd3  10650  faclbnd6  10651  facavg  10653  bcrpcl  10660  bccmpl  10661  fiubm  10735  seq3coll  10749  shftfvalg  10754  shftf  10766  crre  10793  crim  10794  mulreap  10800  readd  10805  resub  10806  remul2  10809  imadd  10813  imsub  10814  immul2  10816  ipcnval  10822  cjsub  10828  cjreim  10839  caucvgre  10917  rexanuz  10924  rexuz3  10926  resqrexlemover  10946  resqrexlemcvg  10955  resqrexlemglsq  10958  sqrtle  10972  sqrtlt  10973  sqrt11ap  10974  sqrt11  10975  absreimsq  11003  absreim  11004  absmul  11005  sqabs  11018  absdiflt  11028  absdifle  11029  abssuble0  11039  abs2difabs  11044  fzomaxdif  11049  caubnd2  11053  rpmaxcl  11159  zmaxcl  11160  minmax  11165  mincl  11166  min1inf  11167  min2inf  11168  minabs  11171  minclpr  11172  rpmincl  11173  2zinfmin  11178  xrmaxrecl  11190  xrminmax  11200  xrmincl  11201  xrmin1inf  11202  xrmin2inf  11203  xrminrecl  11208  xrminrpcl  11209  iooinsup  11212  climconst2  11226  climuni  11228  2clim  11236  climshft  11239  climshft2  11241  cjcn2  11251  climaddc1  11264  climmulc2  11266  climsubc1  11267  climsubc2  11268  climlec2  11276  summodclem2a  11316  zsumdc  11319  isumclim3  11358  mptfzshft  11377  fsumrev  11378  fisum0diag2  11382  telfsumo2  11402  fsumparts  11405  cvgcmpub  11411  binomlem  11418  binom1p  11420  binom1dif  11422  bcxmas  11424  isumshft  11425  expcnvap0  11437  expcnv  11439  geosergap  11441  geolim  11446  cvgratnnlemrate  11465  mertenslemi1  11470  mertenslem2  11471  mertensabs  11472  prodmodc  11513  zproddc  11514  fprodf1o  11523  fprodeq0  11552  efcj  11608  eftlub  11625  effsumlt  11627  efieq  11670  sinsub  11675  cossub  11676  subsin  11678  sinmul  11679  cosmul  11680  addcos  11681  subcos  11682  dvdssub2  11769  dvdsadd  11770  dvdsaddr  11771  dvdssub  11772  dvdssubr  11773  fzocongeq  11790  odd2np1  11804  opoe  11826  omoe  11827  opeo  11828  omeo  11829  divalgb  11856  ndvdsadd  11862  zsupcllemstep  11872  gcdabs  11915  dvdsgcd  11939  absmulgcd  11944  gcdmultiple  11947  gcdmultiplez  11948  rpmulgcd  11953  sqgcd  11956  dvdssqlem  11957  dvdssq  11958  nn0seqcvgd  11967  ialgrlemconst  11969  algrf  11971  algrp1  11972  algcvg  11974  algcvga  11977  lcmval  11989  lcmabs  12002  lcmgcd  12004  lcmdvds  12005  lcmgcdnn  12008  coprmgcdb  12014  coprmdvds  12018  coprmdvds2  12019  qredeq  12022  isprm3  12044  nprm  12049  divgcdodd  12069  prmdvdsexp  12074  sqrt2irr  12088  zgcdsq  12127  hashdvds  12147  phiprmpw  12148  crth  12150  phimullem  12151  modprm0  12180  coprimeprodsq  12183  coprimeprodsq2  12184  pythagtriplem2  12192  pythagtriplem19  12208  pcdvdsb  12245  pcneg  12250  pc2dvds  12255  pc11  12256  pcmpt  12267  pcfac  12274  infpnlem1  12283  prmunb  12286  1arithlem4  12290  1arith  12291  gzaddcl  12301  gzmulcl  12302  gzreim  12303  gzsubcl  12304  4sqlem1  12312  4sqlem4a  12315  4sqlem4  12316  setsvalg  12418  setsfun0  12424  restval  12555  innei  12761  cnovex  12794  txuni2  12854  txbasex  12855  txbas  12856  txtop  12858  txtopon  12860  txss12  12864  txbasval  12865  txcnp  12869  upxp  12870  txcnmpt  12871  uptx  12872  txcn  12873  txrest  12874  txdis  12875  cnmpt21  12889  hmeoco  12914  txhmeo  12917  isxmet2d  12946  blin2  13030  comet  13097  metcn  13112  txmetcn  13117  qtopbasss  13119  qtopbas  13120  remetdval  13137  bl2ioo  13140  blssioo  13143  divcnap  13153  cncfmet  13177  dvaddxxbr  13263  dvcjbr  13270  efle  13295  reapef  13297  sinperlem  13327  sincosq2sgn  13346  sincosq3sgn  13347  sincos6thpi  13361  ioocosf1o  13373  relogoprlem  13387  logleb  13394  cxple3  13439  cxpcom  13455  bj-inex  13682  bj-bdfindis  13722  triap  13801  cvgcmp2nlemabs  13804  trilpolemisumle  13810  inffz  13841
  Copyright terms: Public domain W3C validator