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

Theorem ancoms 264
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 114 . 2  |-  ( ps 
->  ( ph  ->  ch ) )
32imp 122 1  |-  ( ( ps  /\  ph )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem is referenced by:  adantl  271  syl2anr  284  anim12ci  332  sylan9bbr  451  anabss4  544  anabsi7  548  anabsi8  549  im2anan9r  566  bi2anan9r  574  syl3anr2  1227  mp3anr1  1270  mp3anr2  1271  mp3anr3  1272  eu5  1995  2exeu  2040  eqeqan12rd  2104  sylan9eqr  2142  r19.29vva  2513  morex  2797  sylan9ssr  3037  riinm  3797  breqan12rd  3853  elnn  4410  soinxp  4496  seinxp  4497  brelrng  4654  dminss  4833  imainss  4834  funsng  5046  funcnvuni  5069  f1co  5212  f1ocnv  5250  fun11iun  5258  funimass4  5339  fndmdifcom  5389  fsn2  5455  fvtp2g  5488  fvtp3g  5489  fvtp2  5491  fvtp3  5492  acexmid  5633  oveqan12rd  5654  cofunex2g  5865  brtposg  6001  tposoprab  6027  smores3  6040  smores2  6041  smoel  6047  tfri3  6114  rdgtfr  6121  rdgruledefgg  6122  omcl  6204  oeicl  6205  nnmsucr  6231  nnmcom  6232  nndir  6233  nnaordi  6247  nnaordr  6249  nnaword  6250  nnmordi  6255  nnaordex  6266  nnm00  6268  ersym  6284  elecg  6310  riinerm  6345  ecopovsym  6368  ecopovsymg  6371  ecovcom  6379  ecovicom  6380  mapvalg  6395  pmvalg  6396  elpmg  6401  elmapssres  6410  pmss12g  6412  ener  6476  domtr  6482  f1imaeng  6489  fundmen  6503  xpcomco  6522  xpsnen2g  6525  xpdom2  6527  xpdom1g  6529  enen2  6537  domen2  6539  ssfilem  6571  diffitest  6583  fundmfibi  6627  cnvti  6693  djuex  6715  nnnninf  6785  ltsopi  6858  pitric  6859  pitri3or  6860  addcompig  6867  mulcompig  6869  ltapig  6876  ltmpig  6877  nnppipi  6881  addcomnqg  6919  addassnqg  6920  distrnqg  6925  recexnq  6928  nqtri3or  6934  ltmnqg  6939  lt2addnq  6942  lt2mulnq  6943  ltbtwnnqq  6953  prarloclemarch2  6957  enq0ref  6971  distrnq0  6997  mulcomnq0  6998  prcdnql  7022  prcunqu  7023  prarloclemlt  7031  genpassl  7062  genpassu  7063  nqprloc  7083  nqpru  7090  appdiv0nq  7102  addcomprg  7116  mulcomprg  7118  distrlem4prl  7122  distrlem4pru  7123  1idprl  7128  1idpru  7129  ltsopr  7134  recexprlemss1l  7173  recexprlemss1u  7174  gt0srpr  7273  mulcomsrg  7282  ltsosr  7289  aptisr  7303  mulextsr1  7305  axaddcom  7384  axltwlin  7533  axapti  7536  letri3  7545  mul31  7592  cnegexlem3  7638  subval  7653  subcl  7660  pncan2  7668  pncan3  7669  npcan  7670  addsubeq4  7676  npncan3  7699  negsubdi2  7720  muladd  7841  subdi  7842  mulneg2  7853  mulsub  7858  ltleadd  7903  ltsubpos  7911  posdif  7912  addge01  7929  lesub0  7936  reapneg  8050  prodgt02  8286  prodge02  8288  ltdivmul  8309  lerec  8317  lediv2a  8328  le2msq  8334  msq11  8335  lbreu  8378  dfinfre  8389  creur  8391  creui  8392  cju  8393  nnmulcl  8415  nndivtr  8435  avgle1  8626  avgle2  8627  nn0nnaddcl  8674  zletric  8764  zrevaddcl  8770  znnsub  8771  znn0sub  8785  zdclt  8794  zextlt  8808  gtndiv  8811  prime  8815  peano5uzti  8824  uztrn2  9005  uztric  9009  uz11  9010  nn0pzuz  9044  indstr  9050  supinfneg  9052  infsupneg  9053  eluzdc  9066  qrevaddcl  9098  difrp  9139  xrltnsym  9232  xrltso  9235  xrlttri3  9236  xrletri3  9239  xleneg  9268  ixxssixx  9289  iccid  9312  iooshf  9339  iccsupr  9353  iooneg  9374  iccneg  9375  fztri3or  9422  fzdcel  9423  fzn  9425  fzen  9426  fzass4  9444  fzrev  9465  fznn  9470  elfzp1b  9478  elfzm1b  9479  fz0fzdiffz0  9506  difelfznle  9511  fzon  9542  fzonmapblen  9563  eluzgtdifelfzo  9573  ubmelm1fzo  9602  subfzo0  9618  qletric  9620  ioo0  9636  ico0  9638  ioc0  9639  flqbi  9662  flqbi2  9663  flqzadd  9670  modfzo0difsn  9767  fzfig  9802  expcllem  9931  expap0  9950  mulbinom2  10035  expnbnd  10042  sq11ap  10085  hashfacen  10206  shftlem  10215  shftuz  10216  shftfvalg  10217  ovshftex  10218  shftfval  10220  shftval4  10227  shftval5  10228  2shfti  10230  mulreap  10263  sqrt11ap  10436  abs3dif  10503  abs2difabs  10506  maxabslemval  10606  maxle2  10610  maxclpr  10620  climshftlemg  10654  fsumcnv  10794  explecnv  10860  geo2lim  10871  nndivides  10896  0dvds  10909  muldvds1  10914  muldvds2  10915  dvdssubr  10935  dvdsadd2b  10936  odd2np1  10966  mulsucdiv2z  10978  ltoddhalfle  10986  ndvdssub  11023  gcdcom  11058  neggcd  11067  gcdabs2  11074  modgcd  11075  bezoutlemaz  11085  dfgcd2  11096  lcmcom  11139  neglcm  11150  lcmgcdeq  11158  coprmdvds  11167  qredeq  11171  divgcdcoprmex  11177  isprm3  11193  prmind2  11195  dvdsprm  11211  cncongrprm  11229  sqrt2irr  11234  hashgcdeq  11297  uzdcinzz  11355  exmidsbthrlem  11569
  Copyright terms: Public domain W3C validator