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  1327  mp3anr1  1371  mp3anr2  1372  mp3anr3  1373  stoic1b  1473  cbvaldvaw  1979  eu5  2127  2exeu  2172  eqeqan12rd  2248  sylan9eqr  2286  r19.29vva  2679  morex  2991  sylan9ssr  3242  riinm  4048  breqan12rd  4110  elnn  4710  soinxp  4802  seinxp  4803  brelrng  4969  dminss  5158  imainss  5159  funsng  5383  funcnvuni  5406  f1co  5563  f1ocnv  5605  fun11iun  5613  funimass4  5705  fndmdifcom  5762  fsn2  5829  fvtp2g  5871  fvtp3g  5872  fvtp2  5874  fvtp3  5875  riotaeqimp  6006  acexmid  6027  oveqan12rd  6048  cofunex2g  6281  brtposg  6463  tposoprab  6489  smores3  6502  smores2  6503  smoel  6509  tfri3  6576  rdgtfr  6583  rdgruledefgg  6584  omcl  6672  oeicl  6673  nnmsucr  6699  nnmcom  6700  nndir  6701  nnaordi  6719  nnaordr  6721  nnaword  6722  nnmordi  6727  nnaordex  6739  nnm00  6741  ersym  6757  elecg  6785  riinerm  6820  ecopovsym  6843  ecopovsymg  6846  ecovcom  6854  ecovicom  6855  mapvalg  6870  pmvalg  6871  elpmg  6876  elmapssres  6885  pmss12g  6887  ixpconstg  6919  domssr  6994  ener  6996  domtr  7002  f1imaeng  7009  fundmen  7024  xpcomco  7053  xpsnen2g  7056  xpdom2  7058  xpdom1g  7060  enen2  7070  domen2  7072  ssfilem  7105  ssfilemd  7107  diffitest  7119  fiintim  7166  fundmfibi  7180  cnvti  7261  djuex  7285  nnnninf  7368  netap  7516  2omotaplemap  7519  ltsopi  7583  pitric  7584  pitri3or  7585  addcompig  7592  mulcompig  7594  ltapig  7601  ltmpig  7602  nnppipi  7606  addcomnqg  7644  addassnqg  7645  distrnqg  7650  recexnq  7653  nqtri3or  7659  ltmnqg  7664  lt2addnq  7667  lt2mulnq  7668  ltbtwnnqq  7678  prarloclemarch2  7682  enq0ref  7696  distrnq0  7722  mulcomnq0  7723  prcdnql  7747  prcunqu  7748  prarloclemlt  7756  genpassl  7787  genpassu  7788  nqprloc  7808  nqpru  7815  appdiv0nq  7827  addcomprg  7841  mulcomprg  7843  distrlem4prl  7847  distrlem4pru  7848  1idprl  7853  1idpru  7854  ltsopr  7859  recexprlemss1l  7898  recexprlemss1u  7899  gt0srpr  8011  mulcomsrg  8020  ltsosr  8027  aptisr  8042  mulextsr1  8044  map2psrprg  8068  axaddcom  8133  axltwlin  8289  axapti  8292  letri3  8302  eqlelt  8308  mul31  8352  cnegexlem3  8398  subval  8413  subcl  8420  pncan2  8428  pncan3  8429  npcan  8430  addsubeq4  8436  npncan3  8459  negsubdi2  8480  muladd  8605  subdi  8606  mulneg2  8617  mulsub  8622  ltleadd  8668  ltsubpos  8676  posdif  8677  addge01  8694  lesub0  8701  reapneg  8819  prodgt02  9075  prodge02  9077  ltdivmul  9098  lerec  9106  lediv2a  9117  le2msq  9123  msq11  9124  lbreu  9167  dfinfre  9178  creur  9181  creui  9182  cju  9183  nnmulcl  9206  nndivtr  9227  avgle1  9427  avgle2  9428  nn0nnaddcl  9475  zletric  9567  zrevaddcl  9574  znnsub  9575  znn0sub  9589  ltsubnn0  9591  zdclt  9601  zextlt  9616  gtndiv  9619  prime  9623  peano5uzti  9632  uztrn2  9818  uztric  9822  uz11  9823  nn0pzuz  9865  indstr  9871  supinfneg  9873  infsupneg  9874  eluzdc  9888  qrevaddcl  9922  difrp  9971  xrltnsym  10072  xrltso  10075  xrlttri3  10076  xrletri3  10083  xleneg  10116  xaddcom  10140  xposdif  10161  ixxssixx  10181  iccid  10204  iooshf  10231  iccsupr  10245  iooneg  10267  iccneg  10268  fztri3or  10319  fzdcel  10320  fzn  10322  fzen  10323  fzass4  10342  fzrev  10364  fznn  10369  elfzp1b  10377  elfzm1b  10378  fz0fzdiffz0  10410  difelfznle  10415  fzon  10447  fzo0n  10448  fzonmapblen  10472  elfzoextl  10482  eluzgtdifelfzo  10488  ubmelm1fzo  10517  subfzo0  10534  qletric  10547  qdclt  10551  qdcle  10552  ioo0  10565  ico0  10567  ioc0  10568  flqbi  10596  flqbi2  10597  flqzadd  10604  modfzo0difsn  10703  fzfig  10738  expcllem  10858  expap0  10877  mulbinom2  10964  expnbnd  10971  sq11ap  11015  hashfacen  11146  iswrdinn0  11167  ccatsymb  11228  ccatalpha  11239  swrd0g  11290  swrdsbslen  11296  swrdspsleq  11297  wrd2ind  11353  pfxccatin12lem1  11358  pfxccatin12lem2  11361  pfxccatin12  11363  swrdccat3blem  11369  shftlem  11439  shftuz  11440  shftfvalg  11441  ovshftex  11442  shftfval  11444  shftval4  11451  shftval5  11452  2shfti  11454  mulreap  11487  sqrt11ap  11661  abs3dif  11728  abs2difabs  11731  maxabslemval  11831  maxle2  11835  maxclpr  11845  2zsupmax  11849  mingeb  11865  2zinfmin  11866  xrmaxiflemval  11873  xrmax2sup  11877  iooinsup  11900  climshftlemg  11925  fsumcnv  12061  explecnv  12129  geo2lim  12140  prodmodc  12202  fprodcnv  12249  demoivre  12397  demoivreALT  12398  nndivides  12421  0dvds  12435  muldvds1  12440  muldvds2  12441  dvdssubr  12463  dvdsadd2b  12464  odd2np1  12497  mulsucdiv2z  12509  ltoddhalfle  12517  ndvdssub  12554  gcdcom  12607  neggcd  12617  gcdabs2  12624  modgcd  12625  bezoutlemaz  12637  dfgcd2  12648  lcmcom  12699  neglcm  12710  lcmgcdeq  12718  coprmdvds  12727  qredeq  12731  divgcdcoprmex  12737  isprm3  12753  prmind2  12755  dvdsprm  12772  cncongrprm  12792  sqrt2irr  12797  hashgcdeq  12875  modprmn0modprm0  12892  coprimeprodsq  12893  pythagtriplem1  12901  pythagtriplem4  12904  pc2dvds  12966  pc11  12967  pcz  12968  pcprod  12982  prmunb  12998  1arithlem2  13000  1arithlem3  13001  1arith  13003  ptex  13410  issubmnd  13588  submcl  13625  resmhm2b  13635  grpinvsub  13728  dfgrp3mlem  13744  imasabl  13986  mgpress  14008  srgmulgass  14066  dfrhm2  14232  isrim0  14239  rmodislmodlem  14429  rmodislmod  14430  cnfldexp  14656  dvdsrzring  14682  znf1o  14730  eltg  14846  eltg2  14847  tgss  14857  tgss2  14873  basgen2  14875  bastop1  14877  opnneiss  14952  cnrest  15029  txss12  15060  hmeofvalg  15097  txswaphmeolem  15114  txswaphmeo  15115  blpnfctr  15233  metequiv  15289  metcnp3  15305  qtopbasss  15315  reopnap  15340  bl2ioo  15344  ioo2bl  15345  ioo2blex  15346  cncfval  15366  divccncfap  15384  addccncf  15394  expcncf  15403  dvexp  15505  dvmptfsum  15519  dvef  15521  efle  15570  reapef  15572  ptolemy  15618  logleb  15669  lgsprme0  15844  gausslemma2dlem1a  15860  gausslemma2dlem4  15866  lgsquadlem3  15881  2lgsoddprmlem2  15908  upgrpredgv  16070  uhgr2edg  16130  issubgr  16181  subgrprop  16183  subuhgr  16196  subupgr  16197  subumgr  16198  subusgr  16199  upgriswlkdc  16284  upgrwlkvtxedg  16288  g0wlk0  16294  clwwlkn1  16342  clwwlknonex2lem2  16362  uzdcinzz  16499  exmidsbthrlem  16733  triap  16744