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

Theorem ancoms 266
Description: Inference commuting conjunction in antecedent. (Contributed by NM, 21-Apr-1994.)
Hypothesis
Ref Expression
ancoms.1  |-  ( (
ph  /\  ps )  ->  ch )
Assertion
Ref Expression
ancoms  |-  ( ( ps  /\  ph )  ->  ch )

Proof of Theorem ancoms
StepHypRef Expression
1 ancoms.1 . . 3  |-  ( (
ph  /\  ps )  ->  ch )
21expcom 115 . 2  |-  ( ps 
->  ( ph  ->  ch ) )
32imp 123 1  |-  ( ( ps  /\  ph )  ->  ch )
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:  adantl  273  syl2anr  286  anim12ci  335  sylan9bbr  456  anabss4  549  anabsi7  553  anabsi8  554  im2anan9r  571  bi2anan9r  579  syl3anr2  1252  mp3anr1  1295  mp3anr2  1296  mp3anr3  1297  eu5  2022  2exeu  2067  eqeqan12rd  2132  sylan9eqr  2170  r19.29vva  2552  morex  2839  sylan9ssr  3079  riinm  3853  breqan12rd  3914  elnn  4487  soinxp  4577  seinxp  4578  brelrng  4738  dminss  4921  imainss  4922  funsng  5137  funcnvuni  5160  f1co  5308  f1ocnv  5346  fun11iun  5354  funimass4  5438  fndmdifcom  5492  fsn2  5560  fvtp2g  5595  fvtp3g  5596  fvtp2  5598  fvtp3  5599  acexmid  5739  oveqan12rd  5760  cofunex2g  5976  brtposg  6117  tposoprab  6143  smores3  6156  smores2  6157  smoel  6163  tfri3  6230  rdgtfr  6237  rdgruledefgg  6238  omcl  6323  oeicl  6324  nnmsucr  6350  nnmcom  6351  nndir  6352  nnaordi  6370  nnaordr  6372  nnaword  6373  nnmordi  6378  nnaordex  6389  nnm00  6391  ersym  6407  elecg  6433  riinerm  6468  ecopovsym  6491  ecopovsymg  6494  ecovcom  6502  ecovicom  6503  mapvalg  6518  pmvalg  6519  elpmg  6524  elmapssres  6533  pmss12g  6535  ixpconstg  6567  ener  6639  domtr  6645  f1imaeng  6652  fundmen  6666  xpcomco  6686  xpsnen2g  6689  xpdom2  6691  xpdom1g  6693  enen2  6701  domen2  6703  ssfilem  6735  diffitest  6747  fiintim  6783  fundmfibi  6793  cnvti  6872  djuex  6894  nnnninf  6989  ltsopi  7092  pitric  7093  pitri3or  7094  addcompig  7101  mulcompig  7103  ltapig  7110  ltmpig  7111  nnppipi  7115  addcomnqg  7153  addassnqg  7154  distrnqg  7159  recexnq  7162  nqtri3or  7168  ltmnqg  7173  lt2addnq  7176  lt2mulnq  7177  ltbtwnnqq  7187  prarloclemarch2  7191  enq0ref  7205  distrnq0  7231  mulcomnq0  7232  prcdnql  7256  prcunqu  7257  prarloclemlt  7265  genpassl  7296  genpassu  7297  nqprloc  7317  nqpru  7324  appdiv0nq  7336  addcomprg  7350  mulcomprg  7352  distrlem4prl  7356  distrlem4pru  7357  1idprl  7362  1idpru  7363  ltsopr  7368  recexprlemss1l  7407  recexprlemss1u  7408  gt0srpr  7520  mulcomsrg  7529  ltsosr  7536  aptisr  7551  mulextsr1  7553  map2psrprg  7577  axaddcom  7642  axltwlin  7796  axapti  7799  letri3  7809  mul31  7857  cnegexlem3  7903  subval  7918  subcl  7925  pncan2  7933  pncan3  7934  npcan  7935  addsubeq4  7941  npncan3  7964  negsubdi2  7985  muladd  8110  subdi  8111  mulneg2  8122  mulsub  8127  ltleadd  8172  ltsubpos  8180  posdif  8181  addge01  8198  lesub0  8205  reapneg  8322  prodgt02  8568  prodge02  8570  ltdivmul  8591  lerec  8599  lediv2a  8610  le2msq  8616  msq11  8617  lbreu  8660  dfinfre  8671  creur  8674  creui  8675  cju  8676  nnmulcl  8698  nndivtr  8719  avgle1  8911  avgle2  8912  nn0nnaddcl  8959  zletric  9049  zrevaddcl  9055  znnsub  9056  znn0sub  9070  zdclt  9079  zextlt  9094  gtndiv  9097  prime  9101  peano5uzti  9110  uztrn2  9292  uztric  9296  uz11  9297  nn0pzuz  9331  indstr  9337  supinfneg  9339  infsupneg  9340  eluzdc  9353  qrevaddcl  9385  difrp  9426  xrltnsym  9519  xrltso  9522  xrlttri3  9523  xrletri3  9528  xleneg  9560  xaddcom  9584  xposdif  9605  ixxssixx  9625  iccid  9648  iooshf  9675  iccsupr  9689  iooneg  9711  iccneg  9712  fztri3or  9759  fzdcel  9760  fzn  9762  fzen  9763  fzass4  9782  fzrev  9804  fznn  9809  elfzp1b  9817  elfzm1b  9818  fz0fzdiffz0  9847  difelfznle  9852  fzon  9883  fzonmapblen  9904  eluzgtdifelfzo  9914  ubmelm1fzo  9943  subfzo0  9959  qletric  9961  ioo0  9977  ico0  9979  ioc0  9980  flqbi  10003  flqbi2  10004  flqzadd  10011  modfzo0difsn  10108  fzfig  10143  expcllem  10244  expap0  10263  mulbinom2  10348  expnbnd  10355  sq11ap  10398  hashfacen  10519  shftlem  10528  shftuz  10529  shftfvalg  10530  ovshftex  10531  shftfval  10533  shftval4  10540  shftval5  10541  2shfti  10543  mulreap  10576  sqrt11ap  10750  abs3dif  10817  abs2difabs  10820  maxabslemval  10920  maxle2  10924  maxclpr  10934  2zsupmax  10937  xrmaxiflemval  10959  xrmax2sup  10963  iooinsup  10986  climshftlemg  11011  fsumcnv  11146  explecnv  11214  geo2lim  11225  efler  11304  demoivre  11377  demoivreALT  11378  nndivides  11396  0dvds  11409  muldvds1  11414  muldvds2  11415  dvdssubr  11435  dvdsadd2b  11436  odd2np1  11466  mulsucdiv2z  11478  ltoddhalfle  11486  ndvdssub  11523  gcdcom  11558  neggcd  11567  gcdabs2  11574  modgcd  11575  bezoutlemaz  11587  dfgcd2  11598  lcmcom  11641  neglcm  11652  lcmgcdeq  11660  coprmdvds  11669  qredeq  11673  divgcdcoprmex  11679  isprm3  11695  prmind2  11697  dvdsprm  11713  cncongrprm  11731  sqrt2irr  11736  hashgcdeq  11799  eltg  12116  eltg2  12117  tgss  12127  tgss2  12143  basgen2  12145  bastop1  12147  opnneiss  12222  cnrest  12299  txss12  12330  hmeofvalg  12367  txswaphmeolem  12384  txswaphmeo  12385  blpnfctr  12503  metequiv  12559  metcnp3  12575  qtopbasss  12585  reopnap  12602  bl2ioo  12606  ioo2bl  12607  ioo2blex  12608  cncfval  12623  divccncfap  12641  addccncf  12650  expcncf  12656  dvexp  12718  dvef  12730  uzdcinzz  12807  exmidsbthrlem  13019  triap  13026
  Copyright terms: Public domain W3C validator