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  542  anabsi7  546  anabsi8  547  im2anan9r  564  bi2anan9r  572  syl3anr2  1223  mp3anr1  1266  mp3anr2  1267  mp3anr3  1268  eu5  1989  2exeu  2034  eqeqan12rd  2098  sylan9eqr  2136  r19.29vva  2501  morex  2777  sylan9ssr  3014  riinm  3752  breqan12rd  3803  elnn  4348  soinxp  4430  seinxp  4431  brelrng  4587  dminss  4762  imainss  4763  funsng  4970  funcnvuni  4993  f1co  5126  f1ocnv  5164  fun11iun  5172  funimass4  5250  fndmdifcom  5299  fsn2  5363  fvtp2g  5396  fvtp3g  5397  fvtp2  5399  fvtp3  5400  acexmid  5536  oveqan12rd  5557  cofunex2g  5764  brtposg  5897  tposoprab  5923  smores3  5936  smores2  5937  smoel  5943  tfri3  6010  rdgtfr  6017  rdgruledefgg  6018  omcl  6099  oeicl  6100  nnmsucr  6125  nnmcom  6126  nndir  6127  nnaordi  6140  nnaordr  6142  nnaword  6143  nnmordi  6148  nnaordex  6159  nnm00  6161  ersym  6177  elecg  6203  riinerm  6238  ecopovsym  6261  ecopovsymg  6264  ecovcom  6272  ecovicom  6273  ener  6318  domtr  6324  f1imaeng  6331  fundmen  6345  xpcomco  6360  xpsnen2g  6363  xpdom2  6365  xpdom1g  6367  enen2  6372  domen2  6374  ssfilem  6400  diffitest  6411  fundmfibi  6438  cnvti  6481  ltsopi  6561  pitric  6562  pitri3or  6563  addcompig  6570  mulcompig  6572  ltapig  6579  ltmpig  6580  nnppipi  6584  addcomnqg  6622  addassnqg  6623  distrnqg  6628  recexnq  6631  nqtri3or  6637  ltmnqg  6642  lt2addnq  6645  lt2mulnq  6646  ltbtwnnqq  6656  prarloclemarch2  6660  enq0ref  6674  distrnq0  6700  mulcomnq0  6701  prcdnql  6725  prcunqu  6726  prarloclemlt  6734  genpassl  6765  genpassu  6766  nqprloc  6786  nqpru  6793  appdiv0nq  6805  addcomprg  6819  mulcomprg  6821  distrlem4prl  6825  distrlem4pru  6826  1idprl  6831  1idpru  6832  ltsopr  6837  recexprlemss1l  6876  recexprlemss1u  6877  gt0srpr  6976  mulcomsrg  6985  ltsosr  6992  aptisr  7006  mulextsr1  7008  axaddcom  7087  axltwlin  7236  axapti  7239  letri3  7248  mul31  7295  cnegexlem3  7341  subval  7356  subcl  7363  pncan2  7371  pncan3  7372  npcan  7373  addsubeq4  7379  npncan3  7402  negsubdi2  7423  muladd  7544  subdi  7545  mulneg2  7556  mulsub  7561  ltleadd  7606  ltsubpos  7614  posdif  7615  addge01  7632  lesub0  7639  reapneg  7753  prodgt02  7987  prodge02  7989  ltdivmul  8010  lerec  8018  lediv2a  8029  le2msq  8035  msq11  8036  lbreu  8079  dfinfre  8090  creur  8092  creui  8093  cju  8094  nnmulcl  8116  nndivtr  8136  avgle1  8327  avgle2  8328  nn0nnaddcl  8375  zletric  8465  zrevaddcl  8471  znnsub  8472  znn0sub  8486  zdclt  8495  zextlt  8509  gtndiv  8512  prime  8516  peano5uzti  8525  uztrn2  8706  uztric  8710  uz11  8711  nn0pzuz  8745  indstr  8751  supinfneg  8753  infsupneg  8754  eluzdc  8767  qrevaddcl  8799  difrp  8840  xrltnsym  8933  xrltso  8936  xrlttri3  8937  xrletri3  8940  xleneg  8969  ixxssixx  8990  iccid  9013  iooshf  9040  iccsupr  9054  iooneg  9075  iccneg  9076  fztri3or  9123  fzdcel  9124  fzn  9126  fzen  9127  fzass4  9145  fzrev  9166  fznn  9171  elfzp1b  9179  elfzm1b  9180  fz0fzdiffz0  9207  difelfznle  9212  fzon  9241  fzonmapblen  9262  eluzgtdifelfzo  9272  ubmelm1fzo  9301  subfzo0  9317  qletric  9319  ioo0  9335  ico0  9337  ioc0  9338  flqbi  9361  flqbi2  9362  flqzadd  9369  modfzo0difsn  9466  fzfig  9501  expcllem  9573  expap0  9592  mulbinom2  9675  expnbnd  9682  sq11ap  9725  shftlem  9831  shftuz  9832  shftfvalg  9833  ovshftex  9834  shftfval  9836  shftval4  9843  shftval5  9844  2shfti  9846  mulreap  9878  sqrt11ap  10051  abs3dif  10118  abs2difabs  10121  maxabslemval  10221  maxle2  10225  maxclpr  10235  climshftlemg  10268  nndivides  10336  0dvds  10349  muldvds1  10354  muldvds2  10355  dvdssubr  10375  dvdsadd2b  10376  odd2np1  10406  mulsucdiv2z  10418  ltoddhalfle  10426  ndvdssub  10463  gcdcom  10498  neggcd  10507  gcdabs2  10514  modgcd  10515  bezoutlemaz  10525  dfgcd2  10536  lcmcom  10579  neglcm  10590  lcmgcdeq  10598  coprmdvds  10607  qredeq  10611  divgcdcoprmex  10617  isprm3  10633  prmind2  10635  dvdsprm  10651  cncongrprm  10669  sqrt2irr  10674  uzdcinzz  10744
  Copyright terms: Public domain W3C validator