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  579  anabsi7  583  anabsi8  584  im2anan9r  603  bi2anan9r  611  syl3anr2  1326  mp3anr1  1370  mp3anr2  1371  mp3anr3  1372  stoic1b  1472  cbvaldvaw  1979  eu5  2127  2exeu  2172  eqeqan12rd  2248  sylan9eqr  2286  r19.29vva  2678  morex  2990  sylan9ssr  3241  riinm  4043  breqan12rd  4105  elnn  4704  soinxp  4796  seinxp  4797  brelrng  4963  dminss  5151  imainss  5152  funsng  5376  funcnvuni  5399  f1co  5554  f1ocnv  5596  fun11iun  5604  funimass4  5696  fndmdifcom  5753  fsn2  5821  fvtp2g  5863  fvtp3g  5864  fvtp2  5866  fvtp3  5867  riotaeqimp  5996  acexmid  6017  oveqan12rd  6038  cofunex2g  6272  brtposg  6420  tposoprab  6446  smores3  6459  smores2  6460  smoel  6466  tfri3  6533  rdgtfr  6540  rdgruledefgg  6541  omcl  6629  oeicl  6630  nnmsucr  6656  nnmcom  6657  nndir  6658  nnaordi  6676  nnaordr  6678  nnaword  6679  nnmordi  6684  nnaordex  6696  nnm00  6698  ersym  6714  elecg  6742  riinerm  6777  ecopovsym  6800  ecopovsymg  6803  ecovcom  6811  ecovicom  6812  mapvalg  6827  pmvalg  6828  elpmg  6833  elmapssres  6842  pmss12g  6844  ixpconstg  6876  domssr  6951  ener  6953  domtr  6959  f1imaeng  6966  fundmen  6981  xpcomco  7010  xpsnen2g  7013  xpdom2  7015  xpdom1g  7017  enen2  7027  domen2  7029  ssfilem  7062  ssfilemd  7064  diffitest  7076  fiintim  7123  fundmfibi  7137  cnvti  7218  djuex  7242  nnnninf  7325  netap  7473  2omotaplemap  7476  ltsopi  7540  pitric  7541  pitri3or  7542  addcompig  7549  mulcompig  7551  ltapig  7558  ltmpig  7559  nnppipi  7563  addcomnqg  7601  addassnqg  7602  distrnqg  7607  recexnq  7610  nqtri3or  7616  ltmnqg  7621  lt2addnq  7624  lt2mulnq  7625  ltbtwnnqq  7635  prarloclemarch2  7639  enq0ref  7653  distrnq0  7679  mulcomnq0  7680  prcdnql  7704  prcunqu  7705  prarloclemlt  7713  genpassl  7744  genpassu  7745  nqprloc  7765  nqpru  7772  appdiv0nq  7784  addcomprg  7798  mulcomprg  7800  distrlem4prl  7804  distrlem4pru  7805  1idprl  7810  1idpru  7811  ltsopr  7816  recexprlemss1l  7855  recexprlemss1u  7856  gt0srpr  7968  mulcomsrg  7977  ltsosr  7984  aptisr  7999  mulextsr1  8001  map2psrprg  8025  axaddcom  8090  axltwlin  8247  axapti  8250  letri3  8260  eqlelt  8266  mul31  8310  cnegexlem3  8356  subval  8371  subcl  8378  pncan2  8386  pncan3  8387  npcan  8388  addsubeq4  8394  npncan3  8417  negsubdi2  8438  muladd  8563  subdi  8564  mulneg2  8575  mulsub  8580  ltleadd  8626  ltsubpos  8634  posdif  8635  addge01  8652  lesub0  8659  reapneg  8777  prodgt02  9033  prodge02  9035  ltdivmul  9056  lerec  9064  lediv2a  9075  le2msq  9081  msq11  9082  lbreu  9125  dfinfre  9136  creur  9139  creui  9140  cju  9141  nnmulcl  9164  nndivtr  9185  avgle1  9385  avgle2  9386  nn0nnaddcl  9433  zletric  9523  zrevaddcl  9530  znnsub  9531  znn0sub  9545  ltsubnn0  9547  zdclt  9557  zextlt  9572  gtndiv  9575  prime  9579  peano5uzti  9588  uztrn2  9774  uztric  9778  uz11  9779  nn0pzuz  9821  indstr  9827  supinfneg  9829  infsupneg  9830  eluzdc  9844  qrevaddcl  9878  difrp  9927  xrltnsym  10028  xrltso  10031  xrlttri3  10032  xrletri3  10039  xleneg  10072  xaddcom  10096  xposdif  10117  ixxssixx  10137  iccid  10160  iooshf  10187  iccsupr  10201  iooneg  10223  iccneg  10224  fztri3or  10274  fzdcel  10275  fzn  10277  fzen  10278  fzass4  10297  fzrev  10319  fznn  10324  elfzp1b  10332  elfzm1b  10333  fz0fzdiffz0  10365  difelfznle  10370  fzon  10402  fzo0n  10403  fzonmapblen  10427  elfzoextl  10437  eluzgtdifelfzo  10443  ubmelm1fzo  10472  subfzo0  10489  qletric  10502  qdclt  10506  qdcle  10507  ioo0  10520  ico0  10522  ioc0  10523  flqbi  10551  flqbi2  10552  flqzadd  10559  modfzo0difsn  10658  fzfig  10693  expcllem  10813  expap0  10832  mulbinom2  10919  expnbnd  10926  sq11ap  10970  hashfacen  11101  iswrdinn0  11122  ccatsymb  11183  ccatalpha  11194  swrd0g  11245  swrdsbslen  11251  swrdspsleq  11252  wrd2ind  11308  pfxccatin12lem1  11313  pfxccatin12lem2  11316  pfxccatin12  11318  swrdccat3blem  11324  shftlem  11381  shftuz  11382  shftfvalg  11383  ovshftex  11384  shftfval  11386  shftval4  11393  shftval5  11394  2shfti  11396  mulreap  11429  sqrt11ap  11603  abs3dif  11670  abs2difabs  11673  maxabslemval  11773  maxle2  11777  maxclpr  11787  2zsupmax  11791  mingeb  11807  2zinfmin  11808  xrmaxiflemval  11815  xrmax2sup  11819  iooinsup  11842  climshftlemg  11867  fsumcnv  12003  explecnv  12071  geo2lim  12082  prodmodc  12144  fprodcnv  12191  demoivre  12339  demoivreALT  12340  nndivides  12363  0dvds  12377  muldvds1  12382  muldvds2  12383  dvdssubr  12405  dvdsadd2b  12406  odd2np1  12439  mulsucdiv2z  12451  ltoddhalfle  12459  ndvdssub  12496  gcdcom  12549  neggcd  12559  gcdabs2  12566  modgcd  12567  bezoutlemaz  12579  dfgcd2  12590  lcmcom  12641  neglcm  12652  lcmgcdeq  12660  coprmdvds  12669  qredeq  12673  divgcdcoprmex  12679  isprm3  12695  prmind2  12697  dvdsprm  12714  cncongrprm  12734  sqrt2irr  12739  hashgcdeq  12817  modprmn0modprm0  12834  coprimeprodsq  12835  pythagtriplem1  12843  pythagtriplem4  12846  pc2dvds  12908  pc11  12909  pcz  12910  pcprod  12924  prmunb  12940  1arithlem2  12942  1arithlem3  12943  1arith  12945  ptex  13352  issubmnd  13530  submcl  13567  resmhm2b  13577  grpinvsub  13670  dfgrp3mlem  13686  imasabl  13928  mgpress  13950  srgmulgass  14008  dfrhm2  14174  isrim0  14181  rmodislmodlem  14370  rmodislmod  14371  cnfldexp  14597  dvdsrzring  14623  znf1o  14671  eltg  14782  eltg2  14783  tgss  14793  tgss2  14809  basgen2  14811  bastop1  14813  opnneiss  14888  cnrest  14965  txss12  14996  hmeofvalg  15033  txswaphmeolem  15050  txswaphmeo  15051  blpnfctr  15169  metequiv  15225  metcnp3  15241  qtopbasss  15251  reopnap  15276  bl2ioo  15280  ioo2bl  15281  ioo2blex  15282  cncfval  15302  divccncfap  15320  addccncf  15330  expcncf  15339  dvexp  15441  dvmptfsum  15455  dvef  15457  efle  15506  reapef  15508  ptolemy  15554  logleb  15605  lgsprme0  15777  gausslemma2dlem1a  15793  gausslemma2dlem4  15799  lgsquadlem3  15814  2lgsoddprmlem2  15841  upgrpredgv  16003  uhgr2edg  16063  issubgr  16114  subgrprop  16116  subuhgr  16129  subupgr  16130  subumgr  16131  subusgr  16132  upgriswlkdc  16217  upgrwlkvtxedg  16221  g0wlk0  16227  clwwlkn1  16275  clwwlknonex2lem2  16295  uzdcinzz  16420  exmidsbthrlem  16652  triap  16659