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  583  syl2an2r  584  mp3an3an  1321  eqeqan12d  2153  sylan9eq  2190  csbcomg  3020  sylan9ss  3105  ssconb  3204  ineqan12d  3274  dfopg  3698  breqan12d  3940  opexg  4145  copsex2g  4163  ordin  4302  onin  4303  unexg  4359  eusv1  4368  opelvvg  4583  opthprc  4585  opbrop  4613  relop  4684  dmpropg  5006  unixpm  5069  funssres  5160  funinsn  5167  funtp  5171  fnco  5226  resasplitss  5297  fodmrnu  5348  relrnfvex  5432  fconst2g  5628  oveqan12d  5786  ovi3  5900  ovg  5902  f1opw2  5969  off  5987  offres  6026  iunon  6174  nnsucsssuc  6381  nnaword1  6402  ertr  6437  erex  6446  brecop  6512  ecovdi  6533  ecovidi  6534  mapvalg  6545  pmvalg  6546  pmss12g  6562  mapsn  6577  en2sn  6700  xpf1o  6731  xpen  6732  phplem4  6742  ssfilem  6762  diffitest  6774  en1eqsn  6829  sbthlem7  6844  ordiso  6914  updjud  6960  fodju0  7012  finnum  7032  pr2nelem  7040  djucomen  7065  ltsopi  7121  pitric  7122  pitri3or  7123  ltdcpi  7124  mulclpi  7129  addcompig  7130  mulcompig  7132  distrpig  7134  ltexpi  7138  ltapig  7139  ltmpig  7140  dfplpq2  7155  dfmpq2  7156  enqbreq2  7158  enqdc  7162  addcmpblnq  7168  addpipqqslem  7170  mulpipq2  7172  mulpipq  7173  mulpipqqs  7174  addclnq  7176  distrnqg  7188  ltdcnq  7198  ltrnqg  7221  enq0breq  7237  addclnq0  7252  nqnq0a  7255  nqnq0m  7256  nq0m0r  7257  distrnq0  7260  mulcomnq0  7261  genipv  7310  genplt2i  7311  genpelvl  7313  genpelvu  7314  addnqprlemrl  7358  addnqprlemru  7359  addnqprlemfl  7360  addnqprlemfu  7361  addnqpr  7362  mulnqprlemrl  7374  mulnqprlemru  7375  mulnqprlemfl  7376  mulnqprlemfu  7377  mulnqpr  7378  distrlem4prl  7385  distrlem4pru  7386  ltnqpr  7394  recexprlemloc  7432  archrecnq  7464  mulclsr  7555  1idsr  7569  00sr  7570  prsradd  7587  axmulass  7674  axdistr  7675  axcnre  7682  peano5nnnn  7693  mulid1  7756  axltadd  7827  lenlt  7833  cnegexlem3  7932  cnegex  7933  resubcl  8019  subeqrev  8131  muladd  8139  mulsub  8156  mulsub2  8157  ltaddsub2  8192  leaddsub2  8194  leltadd  8202  ltaddpos2  8208  posdif  8210  addge02  8228  mullt0  8235  recexre  8333  recextlem1  8405  recexap  8407  divmuldivap  8465  conjmulap  8482  div2subap  8589  prodgt02  8604  prodge02  8606  lemul2  8608  lemul2a  8610  ltmulgt12  8616  lemulge12  8618  ltmuldiv2  8626  ltdivmul2  8629  ledivmul2  8631  lemuldiv2  8633  negiso  8706  cju  8712  peano5nni  8716  nnaddcl  8733  nnmulcl  8734  nnsub  8752  addltmul  8949  avgle1  8953  avgle2  8954  nnrecl  8968  nn0nnaddcl  9001  zsubcl  9088  zleloe  9094  znnsub  9098  nzadd  9099  zmulcl  9100  zltp1le  9101  zleltp1  9102  nnleltp1  9106  nnltp1le  9107  nnaddm1cl  9108  nn0ltp1le  9109  nn0leltp1  9110  nn0ltlem1  9111  znn0sub  9112  nn0sub  9113  elz2  9115  zapne  9118  zdcle  9120  zdclt  9121  zltlen  9122  nn0lem1lt  9127  nnlem1lt  9128  nnltlem1  9129  zdiv  9132  zextle  9135  zextlt  9136  btwnnz  9138  prime  9143  nneo  9147  peano2uz2  9151  peano5uzti  9152  uzind  9155  fzind  9159  fnn0ind  9160  uzneg  9337  uz11  9341  eluzp1m1  9342  eluzp1p1  9344  uzin  9351  indstr  9381  uz2mulcl  9395  qre  9410  qaddcl  9420  qsubcl  9423  qltlen  9425  qlttri2  9426  irradd  9431  cnref1o  9433  rpaddcl  9458  rpmulcl  9459  rpdivcl  9460  rexadd  9628  rexsub  9629  xaddcom  9637  xnn0xadd0  9643  xnegdi  9644  elicc2  9714  iccshftr  9770  iccshftl  9772  iccdil  9774  icccntr  9776  fzval2  9786  elfz1eq  9808  peano2fzr  9810  fznlem  9814  fzsplit2  9823  fzaddel  9832  fzsubel  9833  fzrev2  9858  fzrev3  9860  uzsplit  9865  fzrevral  9878  fzrevral3  9880  fzshftral  9881  elfz2nn0  9885  fznn0sub2  9898  fz0fzdiffz0  9900  elfzmlbp  9902  difelfzle  9904  difelfznle  9905  1fv  9909  elfzouz2  9931  fzouzsplit  9949  elfzo0le  9955  fzonmapblen  9957  fzofzim  9958  fzoaddel2  9963  eluzgtdifelfzo  9967  elfzodifsumelfzo  9971  ubmelm1fzo  9996  fzofzp1b  9998  fzosplitprm1  10004  fzostep1  10007  subfzo0  10012  qbtwnxr  10028  flqbi2  10057  divfl0  10062  flqzadd  10064  flqmulnn0  10065  addmodidr  10139  modfzo0difsn  10161  frec2uzltd  10169  frec2uzrand  10171  frecfzen2  10193  seq3split  10245  seq3caopr2  10248  exp3vallem  10287  expcllem  10297  expcl2lemap  10298  1exp  10315  expge1  10323  expadd  10328  expmul  10331  expsubap  10334  leexp1a  10341  lt2sq  10359  le2sq  10360  sumsqeq0  10364  bernneq  10405  bernneq2  10406  sq11ap  10451  facdiv  10477  faclbnd  10480  faclbnd3  10482  faclbnd6  10483  facavg  10485  bcrpcl  10492  bccmpl  10493  seq3coll  10578  shftfvalg  10583  shftf  10595  crre  10622  crim  10623  mulreap  10629  readd  10634  resub  10635  remul2  10638  imadd  10642  imsub  10643  immul2  10645  ipcnval  10651  cjsub  10657  cjreim  10668  caucvgre  10746  rexanuz  10753  rexuz3  10755  resqrexlemover  10775  resqrexlemcvg  10784  resqrexlemglsq  10787  sqrtle  10801  sqrtlt  10802  sqrt11ap  10803  sqrt11  10804  absreimsq  10832  absreim  10833  absmul  10834  sqabs  10847  absdiflt  10857  absdifle  10858  abssuble0  10868  abs2difabs  10873  fzomaxdif  10878  caubnd2  10882  rpmaxcl  10988  zmaxcl  10989  minmax  10994  mincl  10995  min1inf  10996  min2inf  10997  minabs  11000  minclpr  11001  rpmincl  11002  xrmaxrecl  11017  xrminmax  11027  xrmincl  11028  xrmin1inf  11029  xrmin2inf  11030  xrminrecl  11035  xrminrpcl  11036  iooinsup  11039  climconst2  11053  climuni  11055  2clim  11063  climshft  11066  climshft2  11068  cjcn2  11078  climaddc1  11091  climmulc2  11093  climsubc1  11094  climsubc2  11095  climlec2  11103  summodclem2a  11143  zsumdc  11146  isumclim3  11185  mptfzshft  11204  fsumrev  11205  fisum0diag2  11209  telfsumo2  11229  fsumparts  11232  cvgcmpub  11238  binomlem  11245  binom1p  11247  binom1dif  11249  bcxmas  11251  isumshft  11252  expcnvap0  11264  expcnv  11266  geosergap  11268  geolim  11273  cvgratnnlemrate  11292  mertenslemi1  11297  mertenslem2  11298  mertensabs  11299  efcj  11368  eftlub  11385  effsumlt  11387  efieq  11431  sinsub  11436  cossub  11437  subsin  11439  sinmul  11440  cosmul  11441  addcos  11442  subcos  11443  dvdssub2  11524  dvdsadd  11525  dvdsaddr  11526  dvdssub  11527  dvdssubr  11528  fzocongeq  11545  odd2np1  11559  opoe  11581  omoe  11582  opeo  11583  omeo  11584  divalgb  11611  ndvdsadd  11617  zsupcllemstep  11627  gcdabs  11665  dvdsgcd  11689  absmulgcd  11694  gcdmultiple  11697  gcdmultiplez  11698  rpmulgcd  11703  sqgcd  11706  dvdssqlem  11707  dvdssq  11708  nn0seqcvgd  11711  ialgrlemconst  11713  algrf  11715  algrp1  11716  algcvg  11718  algcvga  11721  lcmval  11733  lcmabs  11746  lcmgcd  11748  lcmdvds  11749  lcmgcdnn  11752  coprmgcdb  11758  coprmdvds  11762  coprmdvds2  11763  qredeq  11766  isprm3  11788  nprm  11793  divgcdodd  11810  prmdvdsexp  11815  sqrt2irr  11829  zgcdsq  11868  hashdvds  11886  phiprmpw  11887  crth  11889  phimullem  11890  setsvalg  11978  setsfun0  11984  restval  12115  innei  12321  cnovex  12354  txuni2  12414  txbasex  12415  txbas  12416  txtop  12418  txtopon  12420  txss12  12424  txbasval  12425  txcnp  12429  upxp  12430  txcnmpt  12431  uptx  12432  txcn  12433  txrest  12434  txdis  12435  cnmpt21  12449  hmeoco  12474  txhmeo  12477  isxmet2d  12506  blin2  12590  comet  12657  metcn  12672  txmetcn  12677  qtopbasss  12679  qtopbas  12680  remetdval  12697  bl2ioo  12700  blssioo  12703  divcnap  12713  cncfmet  12737  dvaddxxbr  12823  dvcjbr  12830  sinperlem  12878  sincosq2sgn  12897  sincosq3sgn  12898  sincos6thpi  12912  bj-inex  13094  bj-bdfindis  13134  triap  13213  cvgcmp2nlemabs  13216  trilpolemisumle  13220  inffz  13227
  Copyright terms: Public domain W3C validator