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

Step	Hyp	Ref	Expression
1		ancoms.1	. . 3 |- ( ( ph /\ ps ) -> ch )
2	1	expcom 114	. 2 |- ( ps -> ( ph -> ch ) )
3	2	imp 122	1 |- ( ( ps /\ ph ) -> ch )

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  450  anabss4  541  anabsi7  545  anabsi8  546  im2anan9r  563  bi2anan9r  571  syl3anr2  1222  mp3anr1  1265  mp3anr2  1266  mp3anr3  1267  eu5  1988  2exeu  2033  eqeqan12rd  2097  sylan9eqr  2135  r19.29vva  2500  morex  2776  sylan9ssr  3013  riinm  3750  breqan12rd  3801  elnn  4346  soinxp  4428  seinxp  4429  brelrng  4583  dminss  4758  imainss  4759  funsng  4966  funcnvuni  4988  f1co  5121  f1ocnv  5159  fun11iun  5167  funimass4  5245  fndmdifcom  5294  fsn2  5358  fvtp2g  5391  fvtp3g  5392  fvtp2  5394  fvtp3  5395  acexmid  5531  oveqan12rd  5552  cofunex2g  5759  brtposg  5892  tposoprab  5918  smores3  5931  smores2  5932  smoel  5938  tfri3  5976  rdgtfr  5984  rdgruledefgg  5985  omcl  6064  oeicl  6065  nnmsucr  6090  nnmcom  6091  nndir  6092  nnaordi  6104  nnaordr  6106  nnaword  6107  nnmordi  6112  nnaordex  6123  nnm00  6125  ersym  6141  elecg  6167  riinerm  6202  ecopovsym  6225  ecopovsymg  6228  ecovcom  6236  ecovicom  6237  ener  6282  domtr  6288  f1imaeng  6295  fundmen  6309  xpcomco  6323  xpsnen2g  6326  xpdom2  6328  xpdom1g  6330  enen2  6335  domen2  6337  ssfilem  6360  diffitest  6371  fundmfibi  6390  cnvti  6432  ltsopi  6510  pitric  6511  pitri3or  6512  addcompig  6519  mulcompig  6521  ltapig  6528  ltmpig  6529  nnppipi  6533  addcomnqg  6571  addassnqg  6572  distrnqg  6577  recexnq  6580  nqtri3or  6586  ltmnqg  6591  lt2addnq  6594  lt2mulnq  6595  ltbtwnnqq  6605  prarloclemarch2  6609  enq0ref  6623  distrnq0  6649  mulcomnq0  6650  prcdnql  6674  prcunqu  6675  prarloclemlt  6683  genpassl  6714  genpassu  6715  nqprloc  6735  nqpru  6742  appdiv0nq  6754  addcomprg  6768  mulcomprg  6770  distrlem4prl  6774  distrlem4pru  6775  1idprl  6780  1idpru  6781  ltsopr  6786  recexprlemss1l  6825  recexprlemss1u  6826  gt0srpr  6925  mulcomsrg  6934  ltsosr  6941  aptisr  6955  mulextsr1  6957  axaddcom  7036  axltwlin  7180  axapti  7183  letri3  7192  mul31  7239  cnegexlem3  7285  subval  7300  subcl  7307  pncan2  7315  pncan3  7316  npcan  7317  addsubeq4  7323  npncan3  7346  negsubdi2  7367  muladd  7488  subdi  7489  mulneg2  7500  mulsub  7505  ltleadd  7550  ltsubpos  7558  posdif  7559  addge01  7576  lesub0  7583  reapneg  7697  prodgt02  7931  prodge02  7933  ltdivmul  7954  lerec  7962  lediv2a  7973  le2msq  7979  msq11  7980  lbreu  8023  dfinfre  8034  creur  8036  creui  8037  cju  8038  nnmulcl  8060  nndivtr  8080  avgle1  8271  avgle2  8272  nn0nnaddcl  8319  zletric  8395  zrevaddcl  8401  znnsub  8402  znn0sub  8416  zdclt  8425  zextlt  8439  gtndiv  8442  prime  8446  peano5uzti  8455  uztrn2  8636  uztric  8640  uz11  8641  nn0pzuz  8675  indstr  8681  supinfneg  8683  infsupneg  8684  eluzdc  8697  qrevaddcl  8729  difrp  8770  xrltnsym  8868  xrltso  8871  xrlttri3  8872  xrletri3  8875  xleneg  8904  ixxssixx  8925  iccid  8948  iooshf  8975  iccsupr  8989  iooneg  9010  iccneg  9011  fztri3or  9058  fzdcel  9059  fzn  9061  fzen  9062  fzass4  9080  fzrev  9101  fznn  9106  elfzp1b  9114  elfzm1b  9115  fz0fzdiffz0  9141  difelfznle  9146  fzon  9175  fzonmapblen  9196  eluzgtdifelfzo  9206  ubmelm1fzo  9235  subfzo0  9251  qletric  9253  ioo0  9268  ico0  9270  ioc0  9271  flqbi  9292  flqbi2  9293  flqzadd  9300  modfzo0difsn  9397  fzfig  9422  expcllem  9487  expap0  9506  mulbinom2  9589  expnbnd  9596  sq11ap  9639  shftlem  9704  shftuz  9705  shftfvalg  9706  ovshftex  9707  shftfval  9709  shftval4  9716  shftval5  9717  2shfti  9719  mulreap  9751  sqrt11ap  9924  abs3dif  9991  abs2difabs  9994  maxabslemval  10094  maxle2  10098  maxclpr  10108  climshftlemg  10141  nndivides  10202  0dvds  10215  muldvds1  10220  muldvds2  10221  dvdssubr  10241  dvdsadd2b  10242  odd2np1  10272  mulsucdiv2z  10285  ltoddhalfle  10293  ndvdssub  10330  gcdcom  10365  neggcd  10374  gcdabs2  10381  modgcd  10382  bezoutlemaz  10392  dfgcd2  10403  lcmcom  10446  neglcm  10457  lcmgcdeq  10465  coprmdvds  10474  qredeq  10478  divgcdcoprmex  10484  isprm3  10500  prmind2  10502  dvdsprm  10518  cncongrprm  10536  sqrt2irr  10541