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

Theorem ancoms 259
Description: Inference commuting conjunction in antecedent. (Contributed by NM, 21-Apr-1994.)
Hypothesis
Ref Expression
ancoms.1 ((𝜑𝜓) → 𝜒)
Assertion
Ref Expression
ancoms ((𝜓𝜑) → 𝜒)

Proof of Theorem ancoms
StepHypRef Expression
1 ancoms.1 . . 3 ((𝜑𝜓) → 𝜒)
21expcom 113 . 2 (𝜓 → (𝜑𝜒))
32imp 119 1 ((𝜓𝜑) → 𝜒)
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  541  bi2anan9r  549  syl3anr2  1199  mp3anr1  1240  mp3anr2  1241  mp3anr3  1242  eu5  1963  2exeu  2008  eqeqan12rd  2072  sylan9eqr  2110  r19.29vva  2473  morex  2748  sylan9ssr  2987  sspssn  3076  psssstr  3079  riinm  3757  breqan12rd  3808  elnn  4356  soinxp  4438  seinxp  4439  brelrng  4593  dminss  4766  imainss  4767  funsng  4974  funcnvuni  4996  f1co  5129  f1ocnv  5167  fun11iun  5175  funimass4  5252  fndmdifcom  5301  fsn2  5365  fvtp2g  5398  fvtp3g  5399  fvtp2  5401  fvtp3  5402  acexmid  5539  oveqan12rd  5560  cofunex2g  5767  brtposg  5900  tposoprab  5926  smores3  5939  smores2  5940  smoel  5946  tfri3  5984  rdgtfr  5992  rdgruledefgg  5993  omcl  6072  oeicl  6073  nnmsucr  6098  nnmcom  6099  nndir  6100  nnaordi  6112  nnaordr  6114  nnaword  6115  nnmordi  6120  nnaordex  6131  nnm00  6133  ersym  6149  elecg  6175  riinerm  6210  ecopovsym  6233  ecopovsymg  6236  ecovcom  6244  ecovicom  6245  ener  6290  domtr  6296  f1imaeng  6303  fundmen  6317  xpcomco  6331  xpsnen2g  6334  xpdom2  6336  xpdom1g  6338  enen2  6343  domen2  6345  ssfiexmid  6367  diffitest  6375  ltsopi  6476  pitric  6477  pitri3or  6478  addcompig  6485  mulcompig  6487  ltapig  6494  ltmpig  6495  nnppipi  6499  addcomnqg  6537  addassnqg  6538  distrnqg  6543  recexnq  6546  nqtri3or  6552  ltmnqg  6557  lt2addnq  6560  lt2mulnq  6561  ltbtwnnqq  6571  prarloclemarch2  6575  enq0ref  6589  distrnq0  6615  mulcomnq0  6616  prcdnql  6640  prcunqu  6641  prarloclemlt  6649  genpassl  6680  genpassu  6681  nqprloc  6701  nqpru  6708  appdiv0nq  6720  addcomprg  6734  mulcomprg  6736  distrlem4prl  6740  distrlem4pru  6741  1idprl  6746  1idpru  6747  ltsopr  6752  recexprlemss1l  6791  recexprlemss1u  6792  gt0srpr  6891  mulcomsrg  6900  ltsosr  6907  aptisr  6921  mulextsr1  6923  axaddcom  7002  axltwlin  7146  axapti  7149  letri3  7158  mul31  7205  cnegexlem3  7251  subval  7266  subcl  7273  pncan2  7281  pncan3  7282  npcan  7283  addsubeq4  7289  npncan3  7312  negsubdi2  7333  muladd  7453  subdi  7454  mulneg2  7465  mulsub  7470  ltleadd  7515  ltsubpos  7523  posdif  7524  addge01  7541  lesub0  7548  reapneg  7662  prodgt02  7894  prodge02  7896  ltdivmul  7917  lerec  7925  lediv2a  7936  le2msq  7942  msq11  7943  creur  7987  creui  7988  cju  7989  nnmulcl  8011  nndivtr  8031  avgle1  8222  avgle2  8223  nn0nnaddcl  8270  zletric  8346  zrevaddcl  8352  znnsub  8353  znn0sub  8367  zdclt  8376  zextlt  8390  gtndiv  8393  prime  8396  peano5uzti  8405  uztrn2  8586  uztric  8590  uz11  8591  nn0pzuz  8626  indstr  8632  eluzdc  8644  qrevaddcl  8676  difrp  8717  xrltnsym  8815  xrltso  8818  xrlttri3  8819  xrletri3  8822  xleneg  8851  ixxssixx  8872  iccid  8895  iooshf  8922  iccsupr  8936  iooneg  8957  iccneg  8958  fztri3or  9005  fzdcel  9006  fzn  9008  fzen  9009  fzass4  9027  fzrev  9048  fznn  9053  elfzp1b  9061  elfzm1b  9062  fz0fzdiffz0  9089  difelfznle  9095  fzon  9124  fzonmapblen  9145  eluzgtdifelfzo  9155  ubmelm1fzo  9184  subfzo0  9199  qletric  9201  ioo0  9216  ico0  9218  ioc0  9219  flqbi  9240  flqbi2  9241  flqzadd  9248  modfzo0difsn  9345  fzfig  9370  expcllem  9431  expap0  9450  mulbinom2  9533  expnbnd  9540  sq11ap  9583  shftlem  9645  shftuz  9646  shftfvalg  9647  ovshftex  9648  shftfval  9650  shftval4  9657  shftval5  9658  2shfti  9660  mulreap  9692  sqrt11ap  9865  abs3dif  9932  abs2difabs  9935  climshftlemg  10054  nndivides  10115  0dvds  10128  muldvds1  10132  muldvds2  10133  dvdssubr  10153  dvdsadd2b  10154  odd2np1  10184  mulsucdiv2z  10197  ltoddhalfle  10205  ndvdssub  10242  sqrt2irr  10251
  Copyright terms: Public domain W3C validator