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  3197  riinm  3989  breqan12rd  4050  elnn  4642  soinxp  4733  seinxp  4734  brelrng  4897  dminss  5084  imainss  5085  funsng  5304  funcnvuni  5327  f1co  5475  f1ocnv  5517  fun11iun  5525  funimass4  5611  fndmdifcom  5668  fsn2  5736  fvtp2g  5771  fvtp3g  5772  fvtp2  5774  fvtp3  5775  acexmid  5921  oveqan12rd  5942  cofunex2g  6167  brtposg  6312  tposoprab  6338  smores3  6351  smores2  6352  smoel  6358  tfri3  6425  rdgtfr  6432  rdgruledefgg  6433  omcl  6519  oeicl  6520  nnmsucr  6546  nnmcom  6547  nndir  6548  nnaordi  6566  nnaordr  6568  nnaword  6569  nnmordi  6574  nnaordex  6586  nnm00  6588  ersym  6604  elecg  6632  riinerm  6667  ecopovsym  6690  ecopovsymg  6693  ecovcom  6701  ecovicom  6702  mapvalg  6717  pmvalg  6718  elpmg  6723  elmapssres  6732  pmss12g  6734  ixpconstg  6766  ener  6838  domtr  6844  f1imaeng  6851  fundmen  6865  xpcomco  6885  xpsnen2g  6888  xpdom2  6890  xpdom1g  6892  enen2  6902  domen2  6904  ssfilem  6936  diffitest  6948  fiintim  6992  fundmfibi  7004  cnvti  7085  djuex  7109  nnnninf  7192  netap  7321  2omotaplemap  7324  ltsopi  7387  pitric  7388  pitri3or  7389  addcompig  7396  mulcompig  7398  ltapig  7405  ltmpig  7406  nnppipi  7410  addcomnqg  7448  addassnqg  7449  distrnqg  7454  recexnq  7457  nqtri3or  7463  ltmnqg  7468  lt2addnq  7471  lt2mulnq  7472  ltbtwnnqq  7482  prarloclemarch2  7486  enq0ref  7500  distrnq0  7526  mulcomnq0  7527  prcdnql  7551  prcunqu  7552  prarloclemlt  7560  genpassl  7591  genpassu  7592  nqprloc  7612  nqpru  7619  appdiv0nq  7631  addcomprg  7645  mulcomprg  7647  distrlem4prl  7651  distrlem4pru  7652  1idprl  7657  1idpru  7658  ltsopr  7663  recexprlemss1l  7702  recexprlemss1u  7703  gt0srpr  7815  mulcomsrg  7824  ltsosr  7831  aptisr  7846  mulextsr1  7848  map2psrprg  7872  axaddcom  7937  axltwlin  8094  axapti  8097  letri3  8107  eqlelt  8113  mul31  8157  cnegexlem3  8203  subval  8218  subcl  8225  pncan2  8233  pncan3  8234  npcan  8235  addsubeq4  8241  npncan3  8264  negsubdi2  8285  muladd  8410  subdi  8411  mulneg2  8422  mulsub  8427  ltleadd  8473  ltsubpos  8481  posdif  8482  addge01  8499  lesub0  8506  reapneg  8624  prodgt02  8880  prodge02  8882  ltdivmul  8903  lerec  8911  lediv2a  8922  le2msq  8928  msq11  8929  lbreu  8972  dfinfre  8983  creur  8986  creui  8987  cju  8988  nnmulcl  9011  nndivtr  9032  avgle1  9232  avgle2  9233  nn0nnaddcl  9280  zletric  9370  zrevaddcl  9376  znnsub  9377  znn0sub  9391  ltsubnn0  9393  zdclt  9403  zextlt  9418  gtndiv  9421  prime  9425  peano5uzti  9434  uztrn2  9619  uztric  9623  uz11  9624  nn0pzuz  9661  indstr  9667  supinfneg  9669  infsupneg  9670  eluzdc  9684  qrevaddcl  9718  difrp  9767  xrltnsym  9868  xrltso  9871  xrlttri3  9872  xrletri3  9879  xleneg  9912  xaddcom  9936  xposdif  9957  ixxssixx  9977  iccid  10000  iooshf  10027  iccsupr  10041  iooneg  10063  iccneg  10064  fztri3or  10114  fzdcel  10115  fzn  10117  fzen  10118  fzass4  10137  fzrev  10159  fznn  10164  elfzp1b  10172  elfzm1b  10173  fz0fzdiffz0  10205  difelfznle  10210  fzon  10242  fzonmapblen  10263  eluzgtdifelfzo  10273  ubmelm1fzo  10302  subfzo0  10318  qletric  10331  qdclt  10335  qdcle  10336  ioo0  10349  ico0  10351  ioc0  10352  flqbi  10380  flqbi2  10381  flqzadd  10388  modfzo0difsn  10487  fzfig  10522  expcllem  10642  expap0  10661  mulbinom2  10748  expnbnd  10755  sq11ap  10799  hashfacen  10928  iswrdinn0  10940  shftlem  10981  shftuz  10982  shftfvalg  10983  ovshftex  10984  shftfval  10986  shftval4  10993  shftval5  10994  2shfti  10996  mulreap  11029  sqrt11ap  11203  abs3dif  11270  abs2difabs  11273  maxabslemval  11373  maxle2  11377  maxclpr  11387  2zsupmax  11391  mingeb  11407  2zinfmin  11408  xrmaxiflemval  11415  xrmax2sup  11419  iooinsup  11442  climshftlemg  11467  fsumcnv  11602  explecnv  11670  geo2lim  11681  prodmodc  11743  fprodcnv  11790  demoivre  11938  demoivreALT  11939  nndivides  11962  0dvds  11976  muldvds1  11981  muldvds2  11982  dvdssubr  12004  dvdsadd2b  12005  odd2np1  12038  mulsucdiv2z  12050  ltoddhalfle  12058  ndvdssub  12095  gcdcom  12140  neggcd  12150  gcdabs2  12157  modgcd  12158  bezoutlemaz  12170  dfgcd2  12181  lcmcom  12232  neglcm  12243  lcmgcdeq  12251  coprmdvds  12260  qredeq  12264  divgcdcoprmex  12270  isprm3  12286  prmind2  12288  dvdsprm  12305  cncongrprm  12325  sqrt2irr  12330  hashgcdeq  12408  modprmn0modprm0  12425  coprimeprodsq  12426  pythagtriplem1  12434  pythagtriplem4  12437  pc2dvds  12499  pc11  12500  pcz  12501  pcprod  12515  prmunb  12531  1arithlem2  12533  1arithlem3  12534  1arith  12536  ptex  12935  issubmnd  13083  submcl  13111  resmhm2b  13121  grpinvsub  13214  dfgrp3mlem  13230  imasabl  13466  mgpress  13487  srgmulgass  13545  dfrhm2  13710  isrim0  13717  rmodislmodlem  13906  rmodislmod  13907  cnfldexp  14133  dvdsrzring  14159  znf1o  14207  eltg  14288  eltg2  14289  tgss  14299  tgss2  14315  basgen2  14317  bastop1  14319  opnneiss  14394  cnrest  14471  txss12  14502  hmeofvalg  14539  txswaphmeolem  14556  txswaphmeo  14557  blpnfctr  14675  metequiv  14731  metcnp3  14747  qtopbasss  14757  reopnap  14782  bl2ioo  14786  ioo2bl  14787  ioo2blex  14788  cncfval  14808  divccncfap  14826  addccncf  14836  expcncf  14845  dvexp  14947  dvmptfsum  14961  dvef  14963  efle  15012  reapef  15014  ptolemy  15060  logleb  15111  lgsprme0  15283  gausslemma2dlem1a  15299  gausslemma2dlem4  15305  lgsquadlem3  15320  2lgsoddprmlem2  15347  uzdcinzz  15444  exmidsbthrlem  15666  triap  15673