ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ancoms Structured version   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  1187  mp3anr1  1228  mp3anr2  1229  mp3anr3  1230  eu5  1944  2exeu  1989  eqeqan12rd  2053  sylan9eqr  2091  r19.29vva  2450  morex  2719  sylan9ssr  2953  sspssn  3042  psssstr  3045  riinm  3720  breqan12rd  3771  elnn  4271  soinxp  4353  seinxp  4354  brelrng  4508  dminss  4681  imainss  4682  funsng  4889  funcnvuni  4911  f1co  5044  f1ocnv  5082  fun11iun  5090  funimass4  5167  fndmdifcom  5216  fsn2  5280  fvtp2g  5313  fvtp3g  5314  fvtp2  5316  fvtp3  5317  acexmid  5454  oveqan12rd  5475  cofunex2g  5681  brtposg  5810  tposoprab  5836  smores3  5849  smores2  5850  smoel  5856  tfri3  5894  rdgtfr  5901  rdgruledefgg  5902  omcl  5980  oeicl  5981  nnmsucr  6006  nnmcom  6007  nndir  6008  nnaordi  6017  nnaordr  6019  nnaword  6020  nnmordi  6025  nnaordex  6036  nnm00  6038  ersym  6054  elecg  6080  riinerm  6115  ecopovsym  6138  ecopovsymg  6141  ecovcom  6149  ecovicom  6150  ener  6195  domtr  6201  f1imaeng  6208  fundmen  6222  xpcomco  6236  xpsnen2g  6239  xpdom2  6241  xpdom1g  6243  enen2  6248  domen2  6250  ssfiexmid  6254  ltsopi  6304  pitric  6305  pitri3or  6306  addcompig  6313  mulcompig  6315  ltapig  6322  ltmpig  6323  nnppipi  6327  addcomnqg  6365  addassnqg  6366  distrnqg  6371  recexnq  6374  nqtri3or  6380  ltmnqg  6385  lt2addnq  6388  ltbtwnnqq  6398  prarloclemarch2  6402  enq0ref  6415  distrnq0  6441  mulcomnq0  6442  prcdnql  6466  prcunqu  6467  prarloclemlt  6475  genpassl  6506  genpassu  6507  nqprloc  6527  appdiv0nq  6544  addcomprg  6553  mulcomprg  6555  distrlem4prl  6559  distrlem4pru  6560  1idprl  6565  1idpru  6566  ltsopr  6569  recexprlemss1l  6606  recexprlemss1u  6607  gt0srpr  6656  mulcomsrg  6665  ltsosr  6672  aptisr  6685  mulextsr1  6687  axaddcom  6734  axltwlin  6864  axapti  6867  letri3  6876  mul31  6921  cnegexlem3  6965  subval  6980  subcl  6987  pncan2  6995  pncan3  6996  npcan  6997  addsubeq4  7003  npncan3  7025  negsubdi2  7046  muladd  7157  subdi  7158  mulneg2  7169  mulsub  7174  ltleadd  7216  ltsubpos  7224  posdif  7225  addge01  7242  lesub0  7249  reapneg  7361  prodgt02  7580  prodge02  7582  ltdivmul  7603  lerec  7611  lediv2a  7622  le2msq  7628  msq11  7629  creur  7672  creui  7673  cju  7674  nnmulcl  7696  nndivtr  7716  avgle1  7922  avgle2  7923  nn0nnaddcl  7969  zletric  8045  zrevaddcl  8051  znnsub  8052  znn0sub  8065  zdclt  8074  zextlt  8088  gtndiv  8091  prime  8093  peano5uzti  8102  uztrn2  8246  uztric  8250  uz11  8251  nn0pzuz  8286  indstr  8292  eluzdc  8303  qrevaddcl  8333  difrp  8374  xrltnsym  8464  xrltso  8467  xrlttri3  8468  xrletri3  8471  xleneg  8500  ixxssixx  8521  iccid  8544  iooshf  8571  iccsupr  8585  iooneg  8606  iccneg  8607  fztri3or  8653  fzdcel  8654  fzn  8656  fzen  8657  fzass4  8675  fzrev  8696  fznn  8701  elfzp1b  8709  elfzm1b  8710  fz0fzdiffz0  8737  difelfznle  8743  fzon  8772  fzonmapblen  8793  eluzgtdifelfzo  8803  ubmelm1fzo  8832  fzfig  8867  expcllem  8900  expap0  8919  expnbnd  9005  mulreap  9072
  Copyright terms: Public domain W3C validator