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  1346  mp3anr2  1347  mp3anr3  1348  stoic1b  1447  cbvaldvaw  1953  eu5  2100  2exeu  2145  eqeqan12rd  2221  sylan9eqr  2259  r19.29vva  2650  morex  2956  sylan9ssr  3206  riinm  3999  breqan12rd  4060  elnn  4653  soinxp  4744  seinxp  4745  brelrng  4908  dminss  5096  imainss  5097  funsng  5319  funcnvuni  5342  f1co  5492  f1ocnv  5534  fun11iun  5542  funimass4  5628  fndmdifcom  5685  fsn2  5753  fvtp2g  5792  fvtp3g  5793  fvtp2  5795  fvtp3  5796  acexmid  5942  oveqan12rd  5963  cofunex2g  6194  brtposg  6339  tposoprab  6365  smores3  6378  smores2  6379  smoel  6385  tfri3  6452  rdgtfr  6459  rdgruledefgg  6460  omcl  6546  oeicl  6547  nnmsucr  6573  nnmcom  6574  nndir  6575  nnaordi  6593  nnaordr  6595  nnaword  6596  nnmordi  6601  nnaordex  6613  nnm00  6615  ersym  6631  elecg  6659  riinerm  6694  ecopovsym  6717  ecopovsymg  6720  ecovcom  6728  ecovicom  6729  mapvalg  6744  pmvalg  6745  elpmg  6750  elmapssres  6759  pmss12g  6761  ixpconstg  6793  domssr  6868  ener  6870  domtr  6876  f1imaeng  6883  fundmen  6897  xpcomco  6920  xpsnen2g  6923  xpdom2  6925  xpdom1g  6927  enen2  6937  domen2  6939  ssfilem  6971  diffitest  6983  fiintim  7027  fundmfibi  7039  cnvti  7120  djuex  7144  nnnninf  7227  netap  7365  2omotaplemap  7368  ltsopi  7432  pitric  7433  pitri3or  7434  addcompig  7441  mulcompig  7443  ltapig  7450  ltmpig  7451  nnppipi  7455  addcomnqg  7493  addassnqg  7494  distrnqg  7499  recexnq  7502  nqtri3or  7508  ltmnqg  7513  lt2addnq  7516  lt2mulnq  7517  ltbtwnnqq  7527  prarloclemarch2  7531  enq0ref  7545  distrnq0  7571  mulcomnq0  7572  prcdnql  7596  prcunqu  7597  prarloclemlt  7605  genpassl  7636  genpassu  7637  nqprloc  7657  nqpru  7664  appdiv0nq  7676  addcomprg  7690  mulcomprg  7692  distrlem4prl  7696  distrlem4pru  7697  1idprl  7702  1idpru  7703  ltsopr  7708  recexprlemss1l  7747  recexprlemss1u  7748  gt0srpr  7860  mulcomsrg  7869  ltsosr  7876  aptisr  7891  mulextsr1  7893  map2psrprg  7917  axaddcom  7982  axltwlin  8139  axapti  8142  letri3  8152  eqlelt  8158  mul31  8202  cnegexlem3  8248  subval  8263  subcl  8270  pncan2  8278  pncan3  8279  npcan  8280  addsubeq4  8286  npncan3  8309  negsubdi2  8330  muladd  8455  subdi  8456  mulneg2  8467  mulsub  8472  ltleadd  8518  ltsubpos  8526  posdif  8527  addge01  8544  lesub0  8551  reapneg  8669  prodgt02  8925  prodge02  8927  ltdivmul  8948  lerec  8956  lediv2a  8967  le2msq  8973  msq11  8974  lbreu  9017  dfinfre  9028  creur  9031  creui  9032  cju  9033  nnmulcl  9056  nndivtr  9077  avgle1  9277  avgle2  9278  nn0nnaddcl  9325  zletric  9415  zrevaddcl  9422  znnsub  9423  znn0sub  9437  ltsubnn0  9439  zdclt  9449  zextlt  9464  gtndiv  9467  prime  9471  peano5uzti  9480  uztrn2  9665  uztric  9669  uz11  9670  nn0pzuz  9707  indstr  9713  supinfneg  9715  infsupneg  9716  eluzdc  9730  qrevaddcl  9764  difrp  9813  xrltnsym  9914  xrltso  9917  xrlttri3  9918  xrletri3  9925  xleneg  9958  xaddcom  9982  xposdif  10003  ixxssixx  10023  iccid  10046  iooshf  10073  iccsupr  10087  iooneg  10109  iccneg  10110  fztri3or  10160  fzdcel  10161  fzn  10163  fzen  10164  fzass4  10183  fzrev  10205  fznn  10210  elfzp1b  10218  elfzm1b  10219  fz0fzdiffz0  10251  difelfznle  10256  fzon  10288  fzonmapblen  10309  elfzoextl  10318  eluzgtdifelfzo  10324  ubmelm1fzo  10353  subfzo0  10369  qletric  10382  qdclt  10386  qdcle  10387  ioo0  10400  ico0  10402  ioc0  10403  flqbi  10431  flqbi2  10432  flqzadd  10439  modfzo0difsn  10538  fzfig  10573  expcllem  10693  expap0  10712  mulbinom2  10799  expnbnd  10806  sq11ap  10850  hashfacen  10979  iswrdinn0  10997  ccatsymb  11056  shftlem  11069  shftuz  11070  shftfvalg  11071  ovshftex  11072  shftfval  11074  shftval4  11081  shftval5  11082  2shfti  11084  mulreap  11117  sqrt11ap  11291  abs3dif  11358  abs2difabs  11361  maxabslemval  11461  maxle2  11465  maxclpr  11475  2zsupmax  11479  mingeb  11495  2zinfmin  11496  xrmaxiflemval  11503  xrmax2sup  11507  iooinsup  11530  climshftlemg  11555  fsumcnv  11690  explecnv  11758  geo2lim  11769  prodmodc  11831  fprodcnv  11878  demoivre  12026  demoivreALT  12027  nndivides  12050  0dvds  12064  muldvds1  12069  muldvds2  12070  dvdssubr  12092  dvdsadd2b  12093  odd2np1  12126  mulsucdiv2z  12138  ltoddhalfle  12146  ndvdssub  12183  gcdcom  12236  neggcd  12246  gcdabs2  12253  modgcd  12254  bezoutlemaz  12266  dfgcd2  12277  lcmcom  12328  neglcm  12339  lcmgcdeq  12347  coprmdvds  12356  qredeq  12360  divgcdcoprmex  12366  isprm3  12382  prmind2  12384  dvdsprm  12401  cncongrprm  12421  sqrt2irr  12426  hashgcdeq  12504  modprmn0modprm0  12521  coprimeprodsq  12522  pythagtriplem1  12530  pythagtriplem4  12533  pc2dvds  12595  pc11  12596  pcz  12597  pcprod  12611  prmunb  12627  1arithlem2  12629  1arithlem3  12630  1arith  12632  ptex  13038  issubmnd  13216  submcl  13253  resmhm2b  13263  grpinvsub  13356  dfgrp3mlem  13372  imasabl  13614  mgpress  13635  srgmulgass  13693  dfrhm2  13858  isrim0  13865  rmodislmodlem  14054  rmodislmod  14055  cnfldexp  14281  dvdsrzring  14307  znf1o  14355  eltg  14466  eltg2  14467  tgss  14477  tgss2  14493  basgen2  14495  bastop1  14497  opnneiss  14572  cnrest  14649  txss12  14680  hmeofvalg  14717  txswaphmeolem  14734  txswaphmeo  14735  blpnfctr  14853  metequiv  14909  metcnp3  14925  qtopbasss  14935  reopnap  14960  bl2ioo  14964  ioo2bl  14965  ioo2blex  14966  cncfval  14986  divccncfap  15004  addccncf  15014  expcncf  15023  dvexp  15125  dvmptfsum  15139  dvef  15141  efle  15190  reapef  15192  ptolemy  15238  logleb  15289  lgsprme0  15461  gausslemma2dlem1a  15477  gausslemma2dlem4  15483  lgsquadlem3  15498  2lgsoddprmlem2  15525  uzdcinzz  15667  exmidsbthrlem  15894  triap  15901