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

Theorem ancoms 255
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 109 . 2 (𝜓 → (𝜑𝜒))
32imp 115 1 ((𝜓𝜑) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 97
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem is referenced by:  adantl  262  syl2anr  274  anim12ci  322  sylan9bbr  436  anabss4  511  anabsi7  515  anabsi8  516  im2anan9r  531  bi2anan9r  539  syl3anr2  1188  mp3anr1  1229  mp3anr2  1230  mp3anr3  1231  eu5  1947  2exeu  1992  eqeqan12rd  2056  sylan9eqr  2094  r19.29vva  2456  morex  2725  sylan9ssr  2959  sspssn  3048  psssstr  3051  riinm  3729  breqan12rd  3780  elnn  4328  soinxp  4410  seinxp  4411  brelrng  4565  dminss  4738  imainss  4739  funsng  4946  funcnvuni  4968  f1co  5101  f1ocnv  5139  fun11iun  5147  funimass4  5224  fndmdifcom  5273  fsn2  5337  fvtp2g  5370  fvtp3g  5371  fvtp2  5373  fvtp3  5374  acexmid  5511  oveqan12rd  5532  cofunex2g  5739  brtposg  5869  tposoprab  5895  smores3  5908  smores2  5909  smoel  5915  tfri3  5953  rdgtfr  5961  rdgruledefgg  5962  omcl  6041  oeicl  6042  nnmsucr  6067  nnmcom  6068  nndir  6069  nnaordi  6081  nnaordr  6083  nnaword  6084  nnmordi  6089  nnaordex  6100  nnm00  6102  ersym  6118  elecg  6144  riinerm  6179  ecopovsym  6202  ecopovsymg  6205  ecovcom  6213  ecovicom  6214  ener  6259  domtr  6265  f1imaeng  6272  fundmen  6286  xpcomco  6300  xpsnen2g  6303  xpdom2  6305  xpdom1g  6307  enen2  6312  domen2  6314  ssfiexmid  6336  diffitest  6344  ltsopi  6416  pitric  6417  pitri3or  6418  addcompig  6425  mulcompig  6427  ltapig  6434  ltmpig  6435  nnppipi  6439  addcomnqg  6477  addassnqg  6478  distrnqg  6483  recexnq  6486  nqtri3or  6492  ltmnqg  6497  lt2addnq  6500  lt2mulnq  6501  ltbtwnnqq  6511  prarloclemarch2  6515  enq0ref  6529  distrnq0  6555  mulcomnq0  6556  prcdnql  6580  prcunqu  6581  prarloclemlt  6589  genpassl  6620  genpassu  6621  nqprloc  6641  nqpru  6648  appdiv0nq  6660  addcomprg  6674  mulcomprg  6676  distrlem4prl  6680  distrlem4pru  6681  1idprl  6686  1idpru  6687  ltsopr  6692  recexprlemss1l  6731  recexprlemss1u  6732  gt0srpr  6831  mulcomsrg  6840  ltsosr  6847  aptisr  6861  mulextsr1  6863  axaddcom  6942  axltwlin  7085  axapti  7088  letri3  7097  mul31  7142  cnegexlem3  7186  subval  7201  subcl  7208  pncan2  7216  pncan3  7217  npcan  7218  addsubeq4  7224  npncan3  7247  negsubdi2  7268  muladd  7379  subdi  7380  mulneg2  7391  mulsub  7396  ltleadd  7439  ltsubpos  7447  posdif  7448  addge01  7465  lesub0  7472  reapneg  7586  prodgt02  7817  prodge02  7819  ltdivmul  7840  lerec  7848  lediv2a  7859  le2msq  7865  msq11  7866  creur  7909  creui  7910  cju  7911  nnmulcl  7933  nndivtr  7953  avgle1  8163  avgle2  8164  nn0nnaddcl  8211  zletric  8287  zrevaddcl  8293  znnsub  8294  znn0sub  8307  zdclt  8316  zextlt  8330  gtndiv  8333  prime  8335  peano5uzti  8344  uztrn2  8488  uztric  8492  uz11  8493  nn0pzuz  8528  indstr  8534  eluzdc  8545  qrevaddcl  8576  difrp  8617  xrltnsym  8712  xrltso  8715  xrlttri3  8716  xrletri3  8719  xleneg  8748  ixxssixx  8769  iccid  8792  iooshf  8819  iccsupr  8833  iooneg  8854  iccneg  8855  fztri3or  8901  fzdcel  8902  fzn  8904  fzen  8905  fzass4  8923  fzrev  8944  fznn  8949  elfzp1b  8957  elfzm1b  8958  fz0fzdiffz0  8985  difelfznle  8991  fzon  9020  fzonmapblen  9041  eluzgtdifelfzo  9051  ubmelm1fzo  9080  subfzo0  9095  qletric  9097  flqbi  9130  flqbi2  9131  flqzadd  9138  fzfig  9180  expcllem  9240  expap0  9259  expnbnd  9346  sq11ap  9388  shftlem  9391  shftuz  9392  shftfvalg  9393  ovshftex  9394  shftfval  9396  shftval4  9403  shftval5  9404  2shfti  9406  mulreap  9438  sqrt11ap  9610  abs3dif  9675  abs2difabs  9678  climshftlemg  9796  sqrt2irr  9851
  Copyright terms: Public domain W3C validator