Theorem ancoms 268

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

Syntax hints:   -> wi 4   /\ wa 104

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

This theorem is referenced by:  adantl  277  syl2anr  290  anim12ci  339  sylan9bbr  463  anabss4  577  anabsi7  581  anabsi8  582  im2anan9r  599  bi2anan9r  607  syl3anr2  1303  mp3anr1  1347  mp3anr2  1348  mp3anr3  1349  stoic1b  1448  cbvaldvaw  1955  eu5  2102  2exeu  2147  eqeqan12rd  2223  sylan9eqr  2261  r19.29vva  2652  morex  2961  sylan9ssr  3211  riinm  4006  breqan12rd  4068  elnn  4662  soinxp  4753  seinxp  4754  brelrng  4918  dminss  5106  imainss  5107  funsng  5329  funcnvuni  5352  f1co  5505  f1ocnv  5547  fun11iun  5555  funimass4  5642  fndmdifcom  5699  fsn2  5767  fvtp2g  5806  fvtp3g  5807  fvtp2  5809  fvtp3  5810  acexmid  5956  oveqan12rd  5977  cofunex2g  6208  brtposg  6353  tposoprab  6379  smores3  6392  smores2  6393  smoel  6399  tfri3  6466  rdgtfr  6473  rdgruledefgg  6474  omcl  6560  oeicl  6561  nnmsucr  6587  nnmcom  6588  nndir  6589  nnaordi  6607  nnaordr  6609  nnaword  6610  nnmordi  6615  nnaordex  6627  nnm00  6629  ersym  6645  elecg  6673  riinerm  6708  ecopovsym  6731  ecopovsymg  6734  ecovcom  6742  ecovicom  6743  mapvalg  6758  pmvalg  6759  elpmg  6764  elmapssres  6773  pmss12g  6775  ixpconstg  6807  domssr  6882  ener  6884  domtr  6890  f1imaeng  6897  fundmen  6912  xpcomco  6936  xpsnen2g  6939  xpdom2  6941  xpdom1g  6943  enen2  6953  domen2  6955  ssfilem  6987  diffitest  6999  fiintim  7043  fundmfibi  7055  cnvti  7136  djuex  7160  nnnninf  7243  netap  7386  2omotaplemap  7389  ltsopi  7453  pitric  7454  pitri3or  7455  addcompig  7462  mulcompig  7464  ltapig  7471  ltmpig  7472  nnppipi  7476  addcomnqg  7514  addassnqg  7515  distrnqg  7520  recexnq  7523  nqtri3or  7529  ltmnqg  7534  lt2addnq  7537  lt2mulnq  7538  ltbtwnnqq  7548  prarloclemarch2  7552  enq0ref  7566  distrnq0  7592  mulcomnq0  7593  prcdnql  7617  prcunqu  7618  prarloclemlt  7626  genpassl  7657  genpassu  7658  nqprloc  7678  nqpru  7685  appdiv0nq  7697  addcomprg  7711  mulcomprg  7713  distrlem4prl  7717  distrlem4pru  7718  1idprl  7723  1idpru  7724  ltsopr  7729  recexprlemss1l  7768  recexprlemss1u  7769  gt0srpr  7881  mulcomsrg  7890  ltsosr  7897  aptisr  7912  mulextsr1  7914  map2psrprg  7938  axaddcom  8003  axltwlin  8160  axapti  8163  letri3  8173  eqlelt  8179  mul31  8223  cnegexlem3  8269  subval  8284  subcl  8291  pncan2  8299  pncan3  8300  npcan  8301  addsubeq4  8307  npncan3  8330  negsubdi2  8351  muladd  8476  subdi  8477  mulneg2  8488  mulsub  8493  ltleadd  8539  ltsubpos  8547  posdif  8548  addge01  8565  lesub0  8572  reapneg  8690  prodgt02  8946  prodge02  8948  ltdivmul  8969  lerec  8977  lediv2a  8988  le2msq  8994  msq11  8995  lbreu  9038  dfinfre  9049  creur  9052  creui  9053  cju  9054  nnmulcl  9077  nndivtr  9098  avgle1  9298  avgle2  9299  nn0nnaddcl  9346  zletric  9436  zrevaddcl  9443  znnsub  9444  znn0sub  9458  ltsubnn0  9460  zdclt  9470  zextlt  9485  gtndiv  9488  prime  9492  peano5uzti  9501  uztrn2  9686  uztric  9690  uz11  9691  nn0pzuz  9728  indstr  9734  supinfneg  9736  infsupneg  9737  eluzdc  9751  qrevaddcl  9785  difrp  9834  xrltnsym  9935  xrltso  9938  xrlttri3  9939  xrletri3  9946  xleneg  9979  xaddcom  10003  xposdif  10024  ixxssixx  10044  iccid  10067  iooshf  10094  iccsupr  10108  iooneg  10130  iccneg  10131  fztri3or  10181  fzdcel  10182  fzn  10184  fzen  10185  fzass4  10204  fzrev  10226  fznn  10231  elfzp1b  10239  elfzm1b  10240  fz0fzdiffz0  10272  difelfznle  10277  fzon  10309  fzo0n  10310  fzonmapblen  10333  elfzoextl  10342  eluzgtdifelfzo  10348  ubmelm1fzo  10377  subfzo0  10393  qletric  10406  qdclt  10410  qdcle  10411  ioo0  10424  ico0  10426  ioc0  10427  flqbi  10455  flqbi2  10456  flqzadd  10463  modfzo0difsn  10562  fzfig  10597  expcllem  10717  expap0  10736  mulbinom2  10823  expnbnd  10830  sq11ap  10874  hashfacen  11003  iswrdinn0  11021  ccatsymb  11081  swrd0g  11136  swrdsbslen  11142  swrdspsleq  11143  wrd2ind  11199  shftlem  11202  shftuz  11203  shftfvalg  11204  ovshftex  11205  shftfval  11207  shftval4  11214  shftval5  11215  2shfti  11217  mulreap  11250  sqrt11ap  11424  abs3dif  11491  abs2difabs  11494  maxabslemval  11594  maxle2  11598  maxclpr  11608  2zsupmax  11612  mingeb  11628  2zinfmin  11629  xrmaxiflemval  11636  xrmax2sup  11640  iooinsup  11663  climshftlemg  11688  fsumcnv  11823  explecnv  11891  geo2lim  11902  prodmodc  11964  fprodcnv  12011  demoivre  12159  demoivreALT  12160  nndivides  12183  0dvds  12197  muldvds1  12202  muldvds2  12203  dvdssubr  12225  dvdsadd2b  12226  odd2np1  12259  mulsucdiv2z  12271  ltoddhalfle  12279  ndvdssub  12316  gcdcom  12369  neggcd  12379  gcdabs2  12386  modgcd  12387  bezoutlemaz  12399  dfgcd2  12410  lcmcom  12461  neglcm  12472  lcmgcdeq  12480  coprmdvds  12489  qredeq  12493  divgcdcoprmex  12499  isprm3  12515  prmind2  12517  dvdsprm  12534  cncongrprm  12554  sqrt2irr  12559  hashgcdeq  12637  modprmn0modprm0  12654  coprimeprodsq  12655  pythagtriplem1  12663  pythagtriplem4  12666  pc2dvds  12728  pc11  12729  pcz  12730  pcprod  12744  prmunb  12760  1arithlem2  12762  1arithlem3  12763  1arith  12765  ptex  13171  issubmnd  13349  submcl  13386  resmhm2b  13396  grpinvsub  13489  dfgrp3mlem  13505  imasabl  13747  mgpress  13768  srgmulgass  13826  dfrhm2  13991  isrim0  13998  rmodislmodlem  14187  rmodislmod  14188  cnfldexp  14414  dvdsrzring  14440  znf1o  14488  eltg  14599  eltg2  14600  tgss  14610  tgss2  14626  basgen2  14628  bastop1  14630  opnneiss  14705  cnrest  14782  txss12  14813  hmeofvalg  14850  txswaphmeolem  14867  txswaphmeo  14868  blpnfctr  14986  metequiv  15042  metcnp3  15058  qtopbasss  15068  reopnap  15093  bl2ioo  15097  ioo2bl  15098  ioo2blex  15099  cncfval  15119  divccncfap  15137  addccncf  15147  expcncf  15156  dvexp  15258  dvmptfsum  15272  dvef  15274  efle  15323  reapef  15325  ptolemy  15371  logleb  15422  lgsprme0  15594  gausslemma2dlem1a  15610  gausslemma2dlem4  15616  lgsquadlem3  15631  2lgsoddprmlem2  15658  uzdcinzz  15873  exmidsbthrlem  16102  triap  16109