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  275  syl2anr  288  anim12ci  337  sylan9bbr  458  anabss4  551  anabsi7  555  anabsi8  556  im2anan9r  573  bi2anan9r  581  syl3anr2  1254  mp3anr1  1297  mp3anr2  1298  mp3anr3  1299  eu5  2024  2exeu  2069  eqeqan12rd  2134  sylan9eqr  2172  r19.29vva  2554  morex  2841  sylan9ssr  3081  riinm  3855  breqan12rd  3916  elnn  4489  soinxp  4579  seinxp  4580  brelrng  4740  dminss  4923  imainss  4924  funsng  5139  funcnvuni  5162  f1co  5310  f1ocnv  5348  fun11iun  5356  funimass4  5440  fndmdifcom  5494  fsn2  5562  fvtp2g  5597  fvtp3g  5598  fvtp2  5600  fvtp3  5601  acexmid  5741  oveqan12rd  5762  cofunex2g  5978  brtposg  6119  tposoprab  6145  smores3  6158  smores2  6159  smoel  6165  tfri3  6232  rdgtfr  6239  rdgruledefgg  6240  omcl  6325  oeicl  6326  nnmsucr  6352  nnmcom  6353  nndir  6354  nnaordi  6372  nnaordr  6374  nnaword  6375  nnmordi  6380  nnaordex  6391  nnm00  6393  ersym  6409  elecg  6435  riinerm  6470  ecopovsym  6493  ecopovsymg  6496  ecovcom  6504  ecovicom  6505  mapvalg  6520  pmvalg  6521  elpmg  6526  elmapssres  6535  pmss12g  6537  ixpconstg  6569  ener  6641  domtr  6647  f1imaeng  6654  fundmen  6668  xpcomco  6688  xpsnen2g  6691  xpdom2  6693  xpdom1g  6695  enen2  6703  domen2  6705  ssfilem  6737  diffitest  6749  fiintim  6785  fundmfibi  6795  cnvti  6874  djuex  6896  nnnninf  6991  ltsopi  7096  pitric  7097  pitri3or  7098  addcompig  7105  mulcompig  7107  ltapig  7114  ltmpig  7115  nnppipi  7119  addcomnqg  7157  addassnqg  7158  distrnqg  7163  recexnq  7166  nqtri3or  7172  ltmnqg  7177  lt2addnq  7180  lt2mulnq  7181  ltbtwnnqq  7191  prarloclemarch2  7195  enq0ref  7209  distrnq0  7235  mulcomnq0  7236  prcdnql  7260  prcunqu  7261  prarloclemlt  7269  genpassl  7300  genpassu  7301  nqprloc  7321  nqpru  7328  appdiv0nq  7340  addcomprg  7354  mulcomprg  7356  distrlem4prl  7360  distrlem4pru  7361  1idprl  7366  1idpru  7367  ltsopr  7372  recexprlemss1l  7411  recexprlemss1u  7412  gt0srpr  7524  mulcomsrg  7533  ltsosr  7540  aptisr  7555  mulextsr1  7557  map2psrprg  7581  axaddcom  7646  axltwlin  7800  axapti  7803  letri3  7813  mul31  7861  cnegexlem3  7907  subval  7922  subcl  7929  pncan2  7937  pncan3  7938  npcan  7939  addsubeq4  7945  npncan3  7968  negsubdi2  7989  muladd  8114  subdi  8115  mulneg2  8126  mulsub  8131  ltleadd  8176  ltsubpos  8184  posdif  8185  addge01  8202  lesub0  8209  reapneg  8326  prodgt02  8575  prodge02  8577  ltdivmul  8598  lerec  8606  lediv2a  8617  le2msq  8623  msq11  8624  lbreu  8667  dfinfre  8678  creur  8681  creui  8682  cju  8683  nnmulcl  8705  nndivtr  8726  avgle1  8918  avgle2  8919  nn0nnaddcl  8966  zletric  9056  zrevaddcl  9062  znnsub  9063  znn0sub  9077  zdclt  9086  zextlt  9101  gtndiv  9104  prime  9108  peano5uzti  9117  uztrn2  9299  uztric  9303  uz11  9304  nn0pzuz  9338  indstr  9344  supinfneg  9346  infsupneg  9347  eluzdc  9360  qrevaddcl  9392  difrp  9435  xrltnsym  9534  xrltso  9537  xrlttri3  9538  xrletri3  9543  xleneg  9575  xaddcom  9599  xposdif  9620  ixxssixx  9640  iccid  9663  iooshf  9690  iccsupr  9704  iooneg  9726  iccneg  9727  fztri3or  9774  fzdcel  9775  fzn  9777  fzen  9778  fzass4  9797  fzrev  9819  fznn  9824  elfzp1b  9832  elfzm1b  9833  fz0fzdiffz0  9862  difelfznle  9867  fzon  9898  fzonmapblen  9919  eluzgtdifelfzo  9929  ubmelm1fzo  9958  subfzo0  9974  qletric  9976  ioo0  9992  ico0  9994  ioc0  9995  flqbi  10018  flqbi2  10019  flqzadd  10026  modfzo0difsn  10123  fzfig  10158  expcllem  10259  expap0  10278  mulbinom2  10363  expnbnd  10370  sq11ap  10413  hashfacen  10534  shftlem  10543  shftuz  10544  shftfvalg  10545  ovshftex  10546  shftfval  10548  shftval4  10555  shftval5  10556  2shfti  10558  mulreap  10591  sqrt11ap  10765  abs3dif  10832  abs2difabs  10835  maxabslemval  10935  maxle2  10939  maxclpr  10949  2zsupmax  10952  xrmaxiflemval  10974  xrmax2sup  10978  iooinsup  11001  climshftlemg  11026  fsumcnv  11161  explecnv  11229  geo2lim  11240  efler  11319  demoivre  11393  demoivreALT  11394  nndivides  11412  0dvds  11425  muldvds1  11430  muldvds2  11431  dvdssubr  11451  dvdsadd2b  11452  odd2np1  11482  mulsucdiv2z  11494  ltoddhalfle  11502  ndvdssub  11539  gcdcom  11574  neggcd  11583  gcdabs2  11590  modgcd  11591  bezoutlemaz  11603  dfgcd2  11614  lcmcom  11657  neglcm  11668  lcmgcdeq  11676  coprmdvds  11685  qredeq  11689  divgcdcoprmex  11695  isprm3  11711  prmind2  11713  dvdsprm  11729  cncongrprm  11747  sqrt2irr  11752  hashgcdeq  11815  eltg  12132  eltg2  12133  tgss  12143  tgss2  12159  basgen2  12161  bastop1  12163  opnneiss  12238  cnrest  12315  txss12  12346  hmeofvalg  12383  txswaphmeolem  12400  txswaphmeo  12401  blpnfctr  12519  metequiv  12575  metcnp3  12591  qtopbasss  12601  reopnap  12618  bl2ioo  12622  ioo2bl  12623  ioo2blex  12624  cncfval  12639  divccncfap  12657  addccncf  12666  expcncf  12672  dvexp  12755  dvef  12767  ptolemy  12816  uzdcinzz  12901  exmidsbthrlem  13113  triap  13120
  Copyright terms: Public domain W3C validator