Theorem ancoms 266

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 115	. 2 |- ( ps -> ( ph -> ch ) )
3	2	imp 123	1 |- ( ( ps /\ ph ) -> ch )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  adantl  275  syl2anr  288  anim12ci  337  sylan9bbr  458  anabss4  566  anabsi7  570  anabsi8  571  im2anan9r  588  bi2anan9r  596  syl3anr2  1269  mp3anr1  1312  mp3anr2  1313  mp3anr3  1314  eu5  2044  2exeu  2089  eqeqan12rd  2154  sylan9eqr  2192  r19.29vva  2575  morex  2863  sylan9ssr  3106  riinm  3880  breqan12rd  3941  elnn  4514  soinxp  4604  seinxp  4605  brelrng  4765  dminss  4948  imainss  4949  funsng  5164  funcnvuni  5187  f1co  5335  f1ocnv  5373  fun11iun  5381  funimass4  5465  fndmdifcom  5519  fsn2  5587  fvtp2g  5622  fvtp3g  5623  fvtp2  5625  fvtp3  5626  acexmid  5766  oveqan12rd  5787  cofunex2g  6003  brtposg  6144  tposoprab  6170  smores3  6183  smores2  6184  smoel  6190  tfri3  6257  rdgtfr  6264  rdgruledefgg  6265  omcl  6350  oeicl  6351  nnmsucr  6377  nnmcom  6378  nndir  6379  nnaordi  6397  nnaordr  6399  nnaword  6400  nnmordi  6405  nnaordex  6416  nnm00  6418  ersym  6434  elecg  6460  riinerm  6495  ecopovsym  6518  ecopovsymg  6521  ecovcom  6529  ecovicom  6530  mapvalg  6545  pmvalg  6546  elpmg  6551  elmapssres  6560  pmss12g  6562  ixpconstg  6594  ener  6666  domtr  6672  f1imaeng  6679  fundmen  6693  xpcomco  6713  xpsnen2g  6716  xpdom2  6718  xpdom1g  6720  enen2  6728  domen2  6730  ssfilem  6762  diffitest  6774  fiintim  6810  fundmfibi  6820  cnvti  6899  djuex  6921  nnnninf  7016  ltsopi  7121  pitric  7122  pitri3or  7123  addcompig  7130  mulcompig  7132  ltapig  7139  ltmpig  7140  nnppipi  7144  addcomnqg  7182  addassnqg  7183  distrnqg  7188  recexnq  7191  nqtri3or  7197  ltmnqg  7202  lt2addnq  7205  lt2mulnq  7206  ltbtwnnqq  7216  prarloclemarch2  7220  enq0ref  7234  distrnq0  7260  mulcomnq0  7261  prcdnql  7285  prcunqu  7286  prarloclemlt  7294  genpassl  7325  genpassu  7326  nqprloc  7346  nqpru  7353  appdiv0nq  7365  addcomprg  7379  mulcomprg  7381  distrlem4prl  7385  distrlem4pru  7386  1idprl  7391  1idpru  7392  ltsopr  7397  recexprlemss1l  7436  recexprlemss1u  7437  gt0srpr  7549  mulcomsrg  7558  ltsosr  7565  aptisr  7580  mulextsr1  7582  map2psrprg  7606  axaddcom  7671  axltwlin  7825  axapti  7828  letri3  7838  mul31  7886  cnegexlem3  7932  subval  7947  subcl  7954  pncan2  7962  pncan3  7963  npcan  7964  addsubeq4  7970  npncan3  7993  negsubdi2  8014  muladd  8139  subdi  8140  mulneg2  8151  mulsub  8156  ltleadd  8201  ltsubpos  8209  posdif  8210  addge01  8227  lesub0  8234  reapneg  8352  prodgt02  8604  prodge02  8606  ltdivmul  8627  lerec  8635  lediv2a  8646  le2msq  8652  msq11  8653  lbreu  8696  dfinfre  8707  creur  8710  creui  8711  cju  8712  nnmulcl  8734  nndivtr  8755  avgle1  8953  avgle2  8954  nn0nnaddcl  9001  zletric  9091  zrevaddcl  9097  znnsub  9098  znn0sub  9112  zdclt  9121  zextlt  9136  gtndiv  9139  prime  9143  peano5uzti  9152  uztrn2  9336  uztric  9340  uz11  9341  nn0pzuz  9375  indstr  9381  supinfneg  9383  infsupneg  9384  eluzdc  9397  qrevaddcl  9429  difrp  9473  xrltnsym  9572  xrltso  9575  xrlttri3  9576  xrletri3  9581  xleneg  9613  xaddcom  9637  xposdif  9658  ixxssixx  9678  iccid  9701  iooshf  9728  iccsupr  9742  iooneg  9764  iccneg  9765  fztri3or  9812  fzdcel  9813  fzn  9815  fzen  9816  fzass4  9835  fzrev  9857  fznn  9862  elfzp1b  9870  elfzm1b  9871  fz0fzdiffz0  9900  difelfznle  9905  fzon  9936  fzonmapblen  9957  eluzgtdifelfzo  9967  ubmelm1fzo  9996  subfzo0  10012  qletric  10014  ioo0  10030  ico0  10032  ioc0  10033  flqbi  10056  flqbi2  10057  flqzadd  10064  modfzo0difsn  10161  fzfig  10196  expcllem  10297  expap0  10316  mulbinom2  10401  expnbnd  10408  sq11ap  10451  hashfacen  10572  shftlem  10581  shftuz  10582  shftfvalg  10583  ovshftex  10584  shftfval  10586  shftval4  10593  shftval5  10594  2shfti  10596  mulreap  10629  sqrt11ap  10803  abs3dif  10870  abs2difabs  10873  maxabslemval  10973  maxle2  10977  maxclpr  10987  2zsupmax  10990  xrmaxiflemval  11012  xrmax2sup  11016  iooinsup  11039  climshftlemg  11064  fsumcnv  11199  explecnv  11267  geo2lim  11278  efler  11394  demoivre  11468  demoivreALT  11469  nndivides  11489  0dvds  11502  muldvds1  11507  muldvds2  11508  dvdssubr  11528  dvdsadd2b  11529  odd2np1  11559  mulsucdiv2z  11571  ltoddhalfle  11579  ndvdssub  11616  gcdcom  11651  neggcd  11660  gcdabs2  11667  modgcd  11668  bezoutlemaz  11680  dfgcd2  11691  lcmcom  11734  neglcm  11745  lcmgcdeq  11753  coprmdvds  11762  qredeq  11766  divgcdcoprmex  11772  isprm3  11788  prmind2  11790  dvdsprm  11806  cncongrprm  11824  sqrt2irr  11829  hashgcdeq  11893  eltg  12210  eltg2  12211  tgss  12221  tgss2  12237  basgen2  12239  bastop1  12241  opnneiss  12316  cnrest  12393  txss12  12424  hmeofvalg  12461  txswaphmeolem  12478  txswaphmeo  12479  blpnfctr  12597  metequiv  12653  metcnp3  12669  qtopbasss  12679  reopnap  12696  bl2ioo  12700  ioo2bl  12701  ioo2blex  12702  cncfval  12717  divccncfap  12735  addccncf  12744  expcncf  12750  dvexp  12833  dvef  12845  ptolemy  12894  uzdcinzz  12994  exmidsbthrlem  13206  triap  13213