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  601  bi2anan9r  609  syl3anr2  1324  mp3anr1  1368  mp3anr2  1369  mp3anr3  1370  stoic1b  1470  cbvaldvaw  1977  eu5  2125  2exeu  2170  eqeqan12rd  2246  sylan9eqr  2284  r19.29vva  2676  morex  2987  sylan9ssr  3238  riinm  4037  breqan12rd  4099  elnn  4697  soinxp  4788  seinxp  4789  brelrng  4954  dminss  5142  imainss  5143  funsng  5366  funcnvuni  5389  f1co  5542  f1ocnv  5584  fun11iun  5592  funimass4  5683  fndmdifcom  5740  fsn2  5808  fvtp2g  5847  fvtp3g  5848  fvtp2  5850  fvtp3  5851  riotaeqimp  5978  acexmid  5999  oveqan12rd  6020  cofunex2g  6253  brtposg  6398  tposoprab  6424  smores3  6437  smores2  6438  smoel  6444  tfri3  6511  rdgtfr  6518  rdgruledefgg  6519  omcl  6605  oeicl  6606  nnmsucr  6632  nnmcom  6633  nndir  6634  nnaordi  6652  nnaordr  6654  nnaword  6655  nnmordi  6660  nnaordex  6672  nnm00  6674  ersym  6690  elecg  6718  riinerm  6753  ecopovsym  6776  ecopovsymg  6779  ecovcom  6787  ecovicom  6788  mapvalg  6803  pmvalg  6804  elpmg  6809  elmapssres  6818  pmss12g  6820  ixpconstg  6852  domssr  6927  ener  6929  domtr  6935  f1imaeng  6942  fundmen  6957  xpcomco  6981  xpsnen2g  6984  xpdom2  6986  xpdom1g  6988  enen2  6998  domen2  7000  ssfilem  7033  diffitest  7045  fiintim  7089  fundmfibi  7101  cnvti  7182  djuex  7206  nnnninf  7289  netap  7436  2omotaplemap  7439  ltsopi  7503  pitric  7504  pitri3or  7505  addcompig  7512  mulcompig  7514  ltapig  7521  ltmpig  7522  nnppipi  7526  addcomnqg  7564  addassnqg  7565  distrnqg  7570  recexnq  7573  nqtri3or  7579  ltmnqg  7584  lt2addnq  7587  lt2mulnq  7588  ltbtwnnqq  7598  prarloclemarch2  7602  enq0ref  7616  distrnq0  7642  mulcomnq0  7643  prcdnql  7667  prcunqu  7668  prarloclemlt  7676  genpassl  7707  genpassu  7708  nqprloc  7728  nqpru  7735  appdiv0nq  7747  addcomprg  7761  mulcomprg  7763  distrlem4prl  7767  distrlem4pru  7768  1idprl  7773  1idpru  7774  ltsopr  7779  recexprlemss1l  7818  recexprlemss1u  7819  gt0srpr  7931  mulcomsrg  7940  ltsosr  7947  aptisr  7962  mulextsr1  7964  map2psrprg  7988  axaddcom  8053  axltwlin  8210  axapti  8213  letri3  8223  eqlelt  8229  mul31  8273  cnegexlem3  8319  subval  8334  subcl  8341  pncan2  8349  pncan3  8350  npcan  8351  addsubeq4  8357  npncan3  8380  negsubdi2  8401  muladd  8526  subdi  8527  mulneg2  8538  mulsub  8543  ltleadd  8589  ltsubpos  8597  posdif  8598  addge01  8615  lesub0  8622  reapneg  8740  prodgt02  8996  prodge02  8998  ltdivmul  9019  lerec  9027  lediv2a  9038  le2msq  9044  msq11  9045  lbreu  9088  dfinfre  9099  creur  9102  creui  9103  cju  9104  nnmulcl  9127  nndivtr  9148  avgle1  9348  avgle2  9349  nn0nnaddcl  9396  zletric  9486  zrevaddcl  9493  znnsub  9494  znn0sub  9508  ltsubnn0  9510  zdclt  9520  zextlt  9535  gtndiv  9538  prime  9542  peano5uzti  9551  uztrn2  9736  uztric  9740  uz11  9741  nn0pzuz  9778  indstr  9784  supinfneg  9786  infsupneg  9787  eluzdc  9801  qrevaddcl  9835  difrp  9884  xrltnsym  9985  xrltso  9988  xrlttri3  9989  xrletri3  9996  xleneg  10029  xaddcom  10053  xposdif  10074  ixxssixx  10094  iccid  10117  iooshf  10144  iccsupr  10158  iooneg  10180  iccneg  10181  fztri3or  10231  fzdcel  10232  fzn  10234  fzen  10235  fzass4  10254  fzrev  10276  fznn  10281  elfzp1b  10289  elfzm1b  10290  fz0fzdiffz0  10322  difelfznle  10327  fzon  10359  fzo0n  10360  fzonmapblen  10383  elfzoextl  10392  eluzgtdifelfzo  10398  ubmelm1fzo  10427  subfzo0  10443  qletric  10456  qdclt  10460  qdcle  10461  ioo0  10474  ico0  10476  ioc0  10477  flqbi  10505  flqbi2  10506  flqzadd  10513  modfzo0difsn  10612  fzfig  10647  expcllem  10767  expap0  10786  mulbinom2  10873  expnbnd  10880  sq11ap  10924  hashfacen  11053  iswrdinn0  11071  ccatsymb  11132  swrd0g  11187  swrdsbslen  11193  swrdspsleq  11194  wrd2ind  11250  pfxccatin12lem1  11255  pfxccatin12lem2  11258  pfxccatin12  11260  swrdccat3blem  11266  shftlem  11322  shftuz  11323  shftfvalg  11324  ovshftex  11325  shftfval  11327  shftval4  11334  shftval5  11335  2shfti  11337  mulreap  11370  sqrt11ap  11544  abs3dif  11611  abs2difabs  11614  maxabslemval  11714  maxle2  11718  maxclpr  11728  2zsupmax  11732  mingeb  11748  2zinfmin  11749  xrmaxiflemval  11756  xrmax2sup  11760  iooinsup  11783  climshftlemg  11808  fsumcnv  11943  explecnv  12011  geo2lim  12022  prodmodc  12084  fprodcnv  12131  demoivre  12279  demoivreALT  12280  nndivides  12303  0dvds  12317  muldvds1  12322  muldvds2  12323  dvdssubr  12345  dvdsadd2b  12346  odd2np1  12379  mulsucdiv2z  12391  ltoddhalfle  12399  ndvdssub  12436  gcdcom  12489  neggcd  12499  gcdabs2  12506  modgcd  12507  bezoutlemaz  12519  dfgcd2  12530  lcmcom  12581  neglcm  12592  lcmgcdeq  12600  coprmdvds  12609  qredeq  12613  divgcdcoprmex  12619  isprm3  12635  prmind2  12637  dvdsprm  12654  cncongrprm  12674  sqrt2irr  12679  hashgcdeq  12757  modprmn0modprm0  12774  coprimeprodsq  12775  pythagtriplem1  12783  pythagtriplem4  12786  pc2dvds  12848  pc11  12849  pcz  12850  pcprod  12864  prmunb  12880  1arithlem2  12882  1arithlem3  12883  1arith  12885  ptex  13292  issubmnd  13470  submcl  13507  resmhm2b  13517  grpinvsub  13610  dfgrp3mlem  13626  imasabl  13868  mgpress  13889  srgmulgass  13947  dfrhm2  14112  isrim0  14119  rmodislmodlem  14308  rmodislmod  14309  cnfldexp  14535  dvdsrzring  14561  znf1o  14609  eltg  14720  eltg2  14721  tgss  14731  tgss2  14747  basgen2  14749  bastop1  14751  opnneiss  14826  cnrest  14903  txss12  14934  hmeofvalg  14971  txswaphmeolem  14988  txswaphmeo  14989  blpnfctr  15107  metequiv  15163  metcnp3  15179  qtopbasss  15189  reopnap  15214  bl2ioo  15218  ioo2bl  15219  ioo2blex  15220  cncfval  15240  divccncfap  15258  addccncf  15268  expcncf  15277  dvexp  15379  dvmptfsum  15393  dvef  15395  efle  15444  reapef  15446  ptolemy  15492  logleb  15543  lgsprme0  15715  gausslemma2dlem1a  15731  gausslemma2dlem4  15737  lgsquadlem3  15752  2lgsoddprmlem2  15779  upgrpredgv  15938  uhgr2edg  15998  uzdcinzz  16120  exmidsbthrlem  16349  triap  16356