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  1302  mp3anr1  1345  mp3anr2  1346  mp3anr3  1347  stoic1b  1439  cbvaldvaw  1945  eu5  2092  2exeu  2137  eqeqan12rd  2213  sylan9eqr  2251  r19.29vva  2642  morex  2948  sylan9ssr  3198  riinm  3990  breqan12rd  4051  elnn  4643  soinxp  4734  seinxp  4735  brelrng  4898  dminss  5085  imainss  5086  funsng  5305  funcnvuni  5328  f1co  5478  f1ocnv  5520  fun11iun  5528  funimass4  5614  fndmdifcom  5671  fsn2  5739  fvtp2g  5774  fvtp3g  5775  fvtp2  5777  fvtp3  5778  acexmid  5924  oveqan12rd  5945  cofunex2g  6176  brtposg  6321  tposoprab  6347  smores3  6360  smores2  6361  smoel  6367  tfri3  6434  rdgtfr  6441  rdgruledefgg  6442  omcl  6528  oeicl  6529  nnmsucr  6555  nnmcom  6556  nndir  6557  nnaordi  6575  nnaordr  6577  nnaword  6578  nnmordi  6583  nnaordex  6595  nnm00  6597  ersym  6613  elecg  6641  riinerm  6676  ecopovsym  6699  ecopovsymg  6702  ecovcom  6710  ecovicom  6711  mapvalg  6726  pmvalg  6727  elpmg  6732  elmapssres  6741  pmss12g  6743  ixpconstg  6775  ener  6847  domtr  6853  f1imaeng  6860  fundmen  6874  xpcomco  6894  xpsnen2g  6897  xpdom2  6899  xpdom1g  6901  enen2  6911  domen2  6913  ssfilem  6945  diffitest  6957  fiintim  7001  fundmfibi  7013  cnvti  7094  djuex  7118  nnnninf  7201  netap  7337  2omotaplemap  7340  ltsopi  7404  pitric  7405  pitri3or  7406  addcompig  7413  mulcompig  7415  ltapig  7422  ltmpig  7423  nnppipi  7427  addcomnqg  7465  addassnqg  7466  distrnqg  7471  recexnq  7474  nqtri3or  7480  ltmnqg  7485  lt2addnq  7488  lt2mulnq  7489  ltbtwnnqq  7499  prarloclemarch2  7503  enq0ref  7517  distrnq0  7543  mulcomnq0  7544  prcdnql  7568  prcunqu  7569  prarloclemlt  7577  genpassl  7608  genpassu  7609  nqprloc  7629  nqpru  7636  appdiv0nq  7648  addcomprg  7662  mulcomprg  7664  distrlem4prl  7668  distrlem4pru  7669  1idprl  7674  1idpru  7675  ltsopr  7680  recexprlemss1l  7719  recexprlemss1u  7720  gt0srpr  7832  mulcomsrg  7841  ltsosr  7848  aptisr  7863  mulextsr1  7865  map2psrprg  7889  axaddcom  7954  axltwlin  8111  axapti  8114  letri3  8124  eqlelt  8130  mul31  8174  cnegexlem3  8220  subval  8235  subcl  8242  pncan2  8250  pncan3  8251  npcan  8252  addsubeq4  8258  npncan3  8281  negsubdi2  8302  muladd  8427  subdi  8428  mulneg2  8439  mulsub  8444  ltleadd  8490  ltsubpos  8498  posdif  8499  addge01  8516  lesub0  8523  reapneg  8641  prodgt02  8897  prodge02  8899  ltdivmul  8920  lerec  8928  lediv2a  8939  le2msq  8945  msq11  8946  lbreu  8989  dfinfre  9000  creur  9003  creui  9004  cju  9005  nnmulcl  9028  nndivtr  9049  avgle1  9249  avgle2  9250  nn0nnaddcl  9297  zletric  9387  zrevaddcl  9393  znnsub  9394  znn0sub  9408  ltsubnn0  9410  zdclt  9420  zextlt  9435  gtndiv  9438  prime  9442  peano5uzti  9451  uztrn2  9636  uztric  9640  uz11  9641  nn0pzuz  9678  indstr  9684  supinfneg  9686  infsupneg  9687  eluzdc  9701  qrevaddcl  9735  difrp  9784  xrltnsym  9885  xrltso  9888  xrlttri3  9889  xrletri3  9896  xleneg  9929  xaddcom  9953  xposdif  9974  ixxssixx  9994  iccid  10017  iooshf  10044  iccsupr  10058  iooneg  10080  iccneg  10081  fztri3or  10131  fzdcel  10132  fzn  10134  fzen  10135  fzass4  10154  fzrev  10176  fznn  10181  elfzp1b  10189  elfzm1b  10190  fz0fzdiffz0  10222  difelfznle  10227  fzon  10259  fzonmapblen  10280  eluzgtdifelfzo  10290  ubmelm1fzo  10319  subfzo0  10335  qletric  10348  qdclt  10352  qdcle  10353  ioo0  10366  ico0  10368  ioc0  10369  flqbi  10397  flqbi2  10398  flqzadd  10405  modfzo0difsn  10504  fzfig  10539  expcllem  10659  expap0  10678  mulbinom2  10765  expnbnd  10772  sq11ap  10816  hashfacen  10945  iswrdinn0  10957  shftlem  10998  shftuz  10999  shftfvalg  11000  ovshftex  11001  shftfval  11003  shftval4  11010  shftval5  11011  2shfti  11013  mulreap  11046  sqrt11ap  11220  abs3dif  11287  abs2difabs  11290  maxabslemval  11390  maxle2  11394  maxclpr  11404  2zsupmax  11408  mingeb  11424  2zinfmin  11425  xrmaxiflemval  11432  xrmax2sup  11436  iooinsup  11459  climshftlemg  11484  fsumcnv  11619  explecnv  11687  geo2lim  11698  prodmodc  11760  fprodcnv  11807  demoivre  11955  demoivreALT  11956  nndivides  11979  0dvds  11993  muldvds1  11998  muldvds2  11999  dvdssubr  12021  dvdsadd2b  12022  odd2np1  12055  mulsucdiv2z  12067  ltoddhalfle  12075  ndvdssub  12112  gcdcom  12165  neggcd  12175  gcdabs2  12182  modgcd  12183  bezoutlemaz  12195  dfgcd2  12206  lcmcom  12257  neglcm  12268  lcmgcdeq  12276  coprmdvds  12285  qredeq  12289  divgcdcoprmex  12295  isprm3  12311  prmind2  12313  dvdsprm  12330  cncongrprm  12350  sqrt2irr  12355  hashgcdeq  12433  modprmn0modprm0  12450  coprimeprodsq  12451  pythagtriplem1  12459  pythagtriplem4  12462  pc2dvds  12524  pc11  12525  pcz  12526  pcprod  12540  prmunb  12556  1arithlem2  12558  1arithlem3  12559  1arith  12561  ptex  12966  issubmnd  13144  submcl  13181  resmhm2b  13191  grpinvsub  13284  dfgrp3mlem  13300  imasabl  13542  mgpress  13563  srgmulgass  13621  dfrhm2  13786  isrim0  13793  rmodislmodlem  13982  rmodislmod  13983  cnfldexp  14209  dvdsrzring  14235  znf1o  14283  eltg  14372  eltg2  14373  tgss  14383  tgss2  14399  basgen2  14401  bastop1  14403  opnneiss  14478  cnrest  14555  txss12  14586  hmeofvalg  14623  txswaphmeolem  14640  txswaphmeo  14641  blpnfctr  14759  metequiv  14815  metcnp3  14831  qtopbasss  14841  reopnap  14866  bl2ioo  14870  ioo2bl  14871  ioo2blex  14872  cncfval  14892  divccncfap  14910  addccncf  14920  expcncf  14929  dvexp  15031  dvmptfsum  15045  dvef  15047  efle  15096  reapef  15098  ptolemy  15144  logleb  15195  lgsprme0  15367  gausslemma2dlem1a  15383  gausslemma2dlem4  15389  lgsquadlem3  15404  2lgsoddprmlem2  15431  uzdcinzz  15528  exmidsbthrlem  15753  triap  15760