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

Theorem ancoms 259
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 113 . 2  |-  ( ps 
->  ( ph  ->  ch ) )
32imp 119 1  |-  ( ( ps  /\  ph )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem is referenced by:  adantl  266  syl2anr  278  anim12ci  326  sylan9bbr  444  anabss4  519  anabsi7  523  anabsi8  524  im2anan9r  539  bi2anan9r  547  syl3anr2  1197  mp3anr1  1238  mp3anr2  1239  mp3anr3  1240  eu5  1961  2exeu  2006  eqeqan12rd  2070  sylan9eqr  2108  r19.29vva  2471  morex  2745  sylan9ssr  2984  sspssn  3073  psssstr  3076  riinm  3754  breqan12rd  3805  elnn  4353  soinxp  4435  seinxp  4436  brelrng  4590  dminss  4763  imainss  4764  funsng  4971  funcnvuni  4993  f1co  5126  f1ocnv  5164  fun11iun  5172  funimass4  5249  fndmdifcom  5298  fsn2  5362  fvtp2g  5395  fvtp3g  5396  fvtp2  5398  fvtp3  5399  acexmid  5536  oveqan12rd  5557  cofunex2g  5764  brtposg  5897  tposoprab  5923  smores3  5936  smores2  5937  smoel  5943  tfri3  5981  rdgtfr  5989  rdgruledefgg  5990  omcl  6069  oeicl  6070  nnmsucr  6095  nnmcom  6096  nndir  6097  nnaordi  6109  nnaordr  6111  nnaword  6112  nnmordi  6117  nnaordex  6128  nnm00  6130  ersym  6146  elecg  6172  riinerm  6207  ecopovsym  6230  ecopovsymg  6233  ecovcom  6241  ecovicom  6242  ener  6287  domtr  6293  f1imaeng  6300  fundmen  6314  xpcomco  6328  xpsnen2g  6331  xpdom2  6333  xpdom1g  6335  enen2  6340  domen2  6342  ssfiexmid  6364  diffitest  6372  ltsopi  6446  pitric  6447  pitri3or  6448  addcompig  6455  mulcompig  6457  ltapig  6464  ltmpig  6465  nnppipi  6469  addcomnqg  6507  addassnqg  6508  distrnqg  6513  recexnq  6516  nqtri3or  6522  ltmnqg  6527  lt2addnq  6530  lt2mulnq  6531  ltbtwnnqq  6541  prarloclemarch2  6545  enq0ref  6559  distrnq0  6585  mulcomnq0  6586  prcdnql  6610  prcunqu  6611  prarloclemlt  6619  genpassl  6650  genpassu  6651  nqprloc  6671  nqpru  6678  appdiv0nq  6690  addcomprg  6704  mulcomprg  6706  distrlem4prl  6710  distrlem4pru  6711  1idprl  6716  1idpru  6717  ltsopr  6722  recexprlemss1l  6761  recexprlemss1u  6762  gt0srpr  6861  mulcomsrg  6870  ltsosr  6877  aptisr  6891  mulextsr1  6893  axaddcom  6972  axltwlin  7116  axapti  7119  letri3  7128  mul31  7175  cnegexlem3  7221  subval  7236  subcl  7243  pncan2  7251  pncan3  7252  npcan  7253  addsubeq4  7259  npncan3  7282  negsubdi2  7303  muladd  7423  subdi  7424  mulneg2  7435  mulsub  7440  ltleadd  7485  ltsubpos  7493  posdif  7494  addge01  7511  lesub0  7518  reapneg  7632  prodgt02  7864  prodge02  7866  ltdivmul  7887  lerec  7895  lediv2a  7906  le2msq  7912  msq11  7913  creur  7957  creui  7958  cju  7959  nnmulcl  7981  nndivtr  8001  avgle1  8192  avgle2  8193  nn0nnaddcl  8240  zletric  8316  zrevaddcl  8322  znnsub  8323  znn0sub  8337  zdclt  8346  zextlt  8360  gtndiv  8363  prime  8366  peano5uzti  8375  uztrn2  8556  uztric  8560  uz11  8561  nn0pzuz  8596  indstr  8602  eluzdc  8614  qrevaddcl  8646  difrp  8687  xrltnsym  8785  xrltso  8788  xrlttri3  8789  xrletri3  8792  xleneg  8821  ixxssixx  8842  iccid  8865  iooshf  8892  iccsupr  8906  iooneg  8927  iccneg  8928  fztri3or  8975  fzdcel  8976  fzn  8978  fzen  8979  fzass4  8997  fzrev  9018  fznn  9023  elfzp1b  9031  elfzm1b  9032  fz0fzdiffz0  9059  difelfznle  9065  fzon  9094  fzonmapblen  9115  eluzgtdifelfzo  9125  ubmelm1fzo  9154  subfzo0  9169  qletric  9171  flqbi  9205  flqbi2  9206  flqzadd  9213  modfzo0difsn  9310  fzfig  9335  expcllem  9396  expap0  9415  mulbinom2  9497  expnbnd  9504  sq11ap  9547  shftlem  9609  shftuz  9610  shftfvalg  9611  ovshftex  9612  shftfval  9614  shftval4  9621  shftval5  9622  2shfti  9624  mulreap  9656  sqrt11ap  9828  abs3dif  9895  abs2difabs  9898  climshftlemg  10017  nndivides  10078  0dvds  10091  muldvds1  10095  muldvds2  10096  dvdssubr  10116  dvdsadd2b  10117  odd2np1  10147  mulsucdiv2z  10160  ltoddhalfle  10168  sqrt2irr  10194
  Copyright terms: Public domain W3C validator