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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  adantl  277  syl2anr  290  anim12ci  339  sylan9bbr  467  anabss4  583  anabsi7  587  anabsi8  588  im2anan9r  607  bi2anan9r  615  syl3anr2  1331  mp3anr1  1375  mp3anr2  1376  mp3anr3  1377  stoic1b  1477  cbvaldvaw  1986  eu5  2134  2exeu  2179  eqeqan12rd  2255  sylan9eqr  2293  r19.29vva  2696  morex  3010  sylan9ssr  3262  riinm  4085  breqan12rd  4147  elnn  4753  soinxp  4845  seinxp  4846  brelrng  5013  dminss  5202  imainss  5203  funsng  5427  funcnvuni  5450  f1co  5610  f1ocnv  5652  fun11iun  5660  funimass4  5753  fndmdifcom  5815  fsn2  5882  fvtp2g  5924  fvtp3g  5925  fvtp2  5927  fvtp3  5928  riotaeqimp  6063  acexmid  6084  oveqan12rd  6105  cofunex2g  6339  brtposg  6525  tposoprab  6551  smores3  6564  smores2  6565  smoel  6571  tfri3  6638  rdgtfr  6645  rdgruledefgg  6646  omcl  6734  oeicl  6735  nnmsucr  6761  nnmcom  6762  nndir  6763  nnaordi  6781  nnaordr  6783  nnaword  6784  nnmordi  6789  nnaordex  6801  nnm00  6803  ersym  6819  elecg  6847  riinerm  6882  ecopovsym  6905  ecopovsymg  6908  ecovcom  6916  ecovicom  6917  mapvalg  6932  pmvalg  6933  elpmg  6938  elmapssres  6954  pmss12g  6956  ixpconstg  6989  domssr  7064  ener  7066  domtr  7072  f1imaeng  7079  fundmen  7094  xpcomco  7124  xpsnen2g  7127  xpdom2  7129  xpdom1g  7131  enen2  7141  domen2  7143  ssfilem  7177  ssfilemd  7179  diffitest  7191  fiintim  7238  fundmfibi  7252  f1setfi  7317  cnvti  7360  djuex  7384  nnnninf  7467  netap  7621  2omotaplemap  7624  ltsopi  7688  pitric  7689  pitri3or  7690  addcompig  7697  mulcompig  7699  ltapig  7706  ltmpig  7707  nnppipi  7711  addcomnqg  7749  addassnqg  7750  distrnqg  7755  recexnq  7758  nqtri3or  7764  ltmnqg  7769  lt2addnq  7772  lt2mulnq  7773  ltbtwnnqq  7783  prarloclemarch2  7787  enq0ref  7801  distrnq0  7827  mulcomnq0  7828  prcdnql  7852  prcunqu  7853  prarloclemlt  7861  genpassl  7892  genpassu  7893  nqprloc  7913  nqpru  7920  appdiv0nq  7932  addcomprg  7946  mulcomprg  7948  distrlem4prl  7952  distrlem4pru  7953  1idprl  7958  1idpru  7959  ltsopr  7964  recexprlemss1l  8003  recexprlemss1u  8004  gt0srpr  8116  mulcomsrg  8125  ltsosr  8132  aptisr  8147  mulextsr1  8149  map2psrprg  8173  axaddcom  8238  axltwlin  8394  axapti  8397  letri3  8407  eqlelt  8413  mul31  8459  cnegexlem3  8505  subval  8520  subcl  8527  pncan2  8535  pncan3  8536  npcan  8537  addsubeq4  8543  npncan3  8566  negsubdi2  8587  muladd  8713  subdi  8714  mulneg2  8725  mulsub  8730  ltleadd  8776  ltsubpos  8784  posdif  8785  addge01  8802  lesub0  8809  reapneg  8928  prodgt02  9186  prodge02  9188  ltdivmul  9209  lerec  9217  lediv2a  9228  le2msq  9234  msq11  9235  lbreu  9278  dfinfre  9289  creur  9292  creui  9293  cju  9294  indval  9299  nnmulcl  9328  nndivtr  9349  avgle1  9551  avgle2  9552  nn0nnaddcl  9599  zletric  9693  zrevaddcl  9700  znnsub  9701  znn0sub  9715  ltsubnn0  9717  zdclt  9727  zextlt  9743  gtndiv  9746  prime  9750  peano5uzti  9759  uztrn2  9950  uztric  9954  uz11  9955  nn0pzuz  9997  indstr  10003  supinfneg  10005  infsupneg  10006  eluzdc  10020  qrevaddcl  10054  difrp  10104  xrltnsym  10206  xrltso  10209  xrlttri3  10210  xrletri3  10217  xleneg  10250  xaddcom  10274  xposdif  10295  ixxssixx  10315  iccid  10338  iooshf  10365  iccsupr  10379  iooneg  10401  iccneg  10402  fztri3or  10454  fzdcel  10455  fzn  10457  fzen  10458  fzass4  10479  fzrev  10502  fznn  10507  elfzp1b  10515  elfzm1b  10516  fz0fzdiffz0  10548  difelfznle  10553  fzon  10585  fzo0n  10586  fzonmapblen  10610  elfzoextl  10620  eluzgtdifelfzo  10626  ubmelm1fzo  10655  subfzo0  10672  qletric  10687  qdclt  10691  qdcle  10692  ioo0  10705  ico0  10707  ioc0  10708  flqbi  10740  flqbi2  10741  flqzadd  10748  modfzo0difsn  10847  fzfig  10882  expcllem  11002  expap0  11021  mulbinom2  11108  expnbnd  11116  sq11ap  11160  hashfacen  11300  iswrdinn0  11325  ccatsymb  11386  ccatalpha  11397  swrd0g  11448  swrdsbslen  11454  swrdspsleq  11455  wrd2ind  11511  pfxccatin12lem1  11516  pfxccatin12lem2  11519  pfxccatin12  11521  swrdccat3blem  11527  shftlem  11597  shftuz  11598  shftfvalg  11599  ovshftex  11600  shftfval  11602  shftval4  11609  shftval5  11610  2shfti  11612  mulreap  11645  sqrt11ap  11820  abs3dif  11888  abs2difabs  11891  maxabslemval  11991  maxle2  11995  maxclpr  12005  2zsupmax  12009  mingeb  12027  2zinfmin  12028  xrmaxiflemval  12035  xrmax2sup  12039  iooinsup  12062  climshftlemg  12087  fsumcnv  12223  explecnv  12291  geo2lim  12302  prodmodc  12364  fprodcnv  12411  demoivre  12559  demoivreALT  12560  nndivides  12583  0dvds  12597  muldvds1  12602  muldvds2  12603  dvdssubr  12625  dvdsadd2b  12626  odd2np1  12659  mulsucdiv2z  12671  ltoddhalfle  12679  ndvdssub  12716  gcdcom  12769  neggcd  12779  gcdabs2  12786  modgcd  12787  bezoutlemaz  12799  dfgcd2  12810  lcmcom  12861  neglcm  12872  lcmgcdeq  12880  coprmdvds  12889  qredeq  12893  divgcdcoprmex  12899  isprm3  12915  prmind2  12917  dvdsprm  12935  cncongrprm  12955  sqrt2irr  12960  nnmaxpw  12972  hashgcdeq  13041  modprmn0modprm0  13058  coprimeprodsq  13059  pythagtriplem1  13067  pythagtriplem4  13070  pc2dvds  13132  pc11  13133  pcz  13134  pcprod  13148  prmunb  13164  1arithlem2  13166  1arithlem3  13167  1arith  13169  ptex  13671  issubmnd  13808  submcl  13839  resmhm2b  13849  grpinvsub  13940  dfgrp3mlem  13956  cntz2ss  14162  cntzrec  14163  imasabl  14224  mgpress  14314  srgmulgass  14377  dfrhm2  14545  isrim0  14552  rmodislmodlem  14771  rmodislmod  14772  cnfldexp  14998  dvdsrzring  15022  znf1o  15070  eltg  15244  eltg2  15245  tgss  15255  tgss2  15271  basgen2  15273  bastop1  15275  opnneiss  15350  cnrest  15427  txss12  15458  hmeofvalg  15495  txswaphmeolem  15512  txswaphmeo  15513  blpnfctr  15631  metequiv  15687  metcnp3  15703  qtopbasss  15713  reopnap  15738  bl2ioo  15742  ioo2bl  15743  ioo2blex  15744  cncfval  15764  divccncfap  15782  addccncf  15792  expcncf  15801  dvexp  15903  dvmptfsum  15917  dvef  15919  efle  15968  reapef  15970  ptolemy  16017  logleb  16069  logdivle  16089  lgsprme0  16327  gausslemma2dlem1a  16343  gausslemma2dlem4  16349  lgsquadlem3  16364  2lgsoddprmlem2  16391  upgrpredgv  16553  uhgr2edg  16613  issubgr  16664  subgrprop  16666  subuhgr  16679  subupgr  16680  subumgr  16681  subusgr  16682  upgriswlkdc  16767  upgrwlkvtxedg  16771  g0wlk0  16777  clwwlkn1  16825  clwwlknonex2lem2  16845  dichmul0orlem3  16921  uzdcinzz  16992  exmidsbthrlem  17233  triap  17244