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  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  4080  breqan12rd  4142  elnn  4748  soinxp  4840  seinxp  4841  brelrng  5008  dminss  5197  imainss  5198  funsng  5422  funcnvuni  5445  f1co  5605  f1ocnv  5647  fun11iun  5655  funimass4  5747  fndmdifcom  5806  fsn2  5873  fvtp2g  5915  fvtp3g  5916  fvtp2  5918  fvtp3  5919  riotaeqimp  6053  acexmid  6074  oveqan12rd  6095  cofunex2g  6329  brtposg  6515  tposoprab  6541  smores3  6554  smores2  6555  smoel  6561  tfri3  6628  rdgtfr  6635  rdgruledefgg  6636  omcl  6724  oeicl  6725  nnmsucr  6751  nnmcom  6752  nndir  6753  nnaordi  6771  nnaordr  6773  nnaword  6774  nnmordi  6779  nnaordex  6791  nnm00  6793  ersym  6809  elecg  6837  riinerm  6872  ecopovsym  6895  ecopovsymg  6898  ecovcom  6906  ecovicom  6907  mapvalg  6922  pmvalg  6923  elpmg  6928  elmapssres  6944  pmss12g  6946  ixpconstg  6979  domssr  7054  ener  7056  domtr  7062  f1imaeng  7069  fundmen  7084  xpcomco  7114  xpsnen2g  7117  xpdom2  7119  xpdom1g  7121  enen2  7131  domen2  7133  ssfilem  7167  ssfilemd  7169  diffitest  7181  fiintim  7228  fundmfibi  7242  f1setfi  7307  cnvti  7349  djuex  7373  nnnninf  7456  netap  7610  2omotaplemap  7613  ltsopi  7677  pitric  7678  pitri3or  7679  addcompig  7686  mulcompig  7688  ltapig  7695  ltmpig  7696  nnppipi  7700  addcomnqg  7738  addassnqg  7739  distrnqg  7744  recexnq  7747  nqtri3or  7753  ltmnqg  7758  lt2addnq  7761  lt2mulnq  7762  ltbtwnnqq  7772  prarloclemarch2  7776  enq0ref  7790  distrnq0  7816  mulcomnq0  7817  prcdnql  7841  prcunqu  7842  prarloclemlt  7850  genpassl  7881  genpassu  7882  nqprloc  7902  nqpru  7909  appdiv0nq  7921  addcomprg  7935  mulcomprg  7937  distrlem4prl  7941  distrlem4pru  7942  1idprl  7947  1idpru  7948  ltsopr  7953  recexprlemss1l  7992  recexprlemss1u  7993  gt0srpr  8105  mulcomsrg  8114  ltsosr  8121  aptisr  8136  mulextsr1  8138  map2psrprg  8162  axaddcom  8227  axltwlin  8383  axapti  8386  letri3  8396  eqlelt  8402  mul31  8447  cnegexlem3  8493  subval  8508  subcl  8515  pncan2  8523  pncan3  8524  npcan  8525  addsubeq4  8531  npncan3  8554  negsubdi2  8575  muladd  8701  subdi  8702  mulneg2  8713  mulsub  8718  ltleadd  8764  ltsubpos  8772  posdif  8773  addge01  8790  lesub0  8797  reapneg  8915  prodgt02  9173  prodge02  9175  ltdivmul  9196  lerec  9204  lediv2a  9215  le2msq  9221  msq11  9222  lbreu  9265  dfinfre  9276  creur  9279  creui  9280  cju  9281  nnmulcl  9304  nndivtr  9325  avgle1  9525  avgle2  9526  nn0nnaddcl  9573  zletric  9667  zrevaddcl  9674  znnsub  9675  znn0sub  9689  ltsubnn0  9691  zdclt  9701  zextlt  9717  gtndiv  9720  prime  9724  peano5uzti  9733  uztrn2  9919  uztric  9923  uz11  9924  nn0pzuz  9966  indstr  9972  supinfneg  9974  infsupneg  9975  eluzdc  9989  qrevaddcl  10023  difrp  10072  xrltnsym  10174  xrltso  10177  xrlttri3  10178  xrletri3  10185  xleneg  10218  xaddcom  10242  xposdif  10263  ixxssixx  10283  iccid  10306  iooshf  10333  iccsupr  10347  iooneg  10369  iccneg  10370  fztri3or  10422  fzdcel  10423  fzn  10425  fzen  10426  fzass4  10446  fzrev  10469  fznn  10474  elfzp1b  10482  elfzm1b  10483  fz0fzdiffz0  10515  difelfznle  10520  fzon  10552  fzo0n  10553  fzonmapblen  10577  elfzoextl  10587  eluzgtdifelfzo  10593  ubmelm1fzo  10622  subfzo0  10639  qletric  10654  qdclt  10658  qdcle  10659  ioo0  10672  ico0  10674  ioc0  10675  flqbi  10703  flqbi2  10704  flqzadd  10711  modfzo0difsn  10810  fzfig  10845  expcllem  10965  expap0  10984  mulbinom2  11071  expnbnd  11079  sq11ap  11123  hashfacen  11262  iswrdinn0  11287  ccatsymb  11348  ccatalpha  11359  swrd0g  11410  swrdsbslen  11416  swrdspsleq  11417  wrd2ind  11473  pfxccatin12lem1  11478  pfxccatin12lem2  11481  pfxccatin12  11483  swrdccat3blem  11489  shftlem  11559  shftuz  11560  shftfvalg  11561  ovshftex  11562  shftfval  11564  shftval4  11571  shftval5  11572  2shfti  11574  mulreap  11607  sqrt11ap  11782  abs3dif  11849  abs2difabs  11852  maxabslemval  11952  maxle2  11956  maxclpr  11966  2zsupmax  11970  mingeb  11986  2zinfmin  11987  xrmaxiflemval  11994  xrmax2sup  11998  iooinsup  12021  climshftlemg  12046  fsumcnv  12182  explecnv  12250  geo2lim  12261  prodmodc  12323  fprodcnv  12370  demoivre  12518  demoivreALT  12519  nndivides  12542  0dvds  12556  muldvds1  12561  muldvds2  12562  dvdssubr  12584  dvdsadd2b  12585  odd2np1  12618  mulsucdiv2z  12630  ltoddhalfle  12638  ndvdssub  12675  gcdcom  12728  neggcd  12738  gcdabs2  12745  modgcd  12746  bezoutlemaz  12758  dfgcd2  12769  lcmcom  12820  neglcm  12831  lcmgcdeq  12839  coprmdvds  12848  qredeq  12852  divgcdcoprmex  12858  isprm3  12874  prmind2  12876  dvdsprm  12893  cncongrprm  12913  sqrt2irr  12918  hashgcdeq  12996  modprmn0modprm0  13013  coprimeprodsq  13014  pythagtriplem1  13022  pythagtriplem4  13025  pc2dvds  13087  pc11  13088  pcz  13089  pcprod  13103  prmunb  13119  1arithlem2  13121  1arithlem3  13122  1arith  13124  ptex  13595  issubmnd  13732  submcl  13763  resmhm2b  13773  grpinvsub  13864  dfgrp3mlem  13880  imasabl  14117  mgpress  14205  srgmulgass  14267  dfrhm2  14434  isrim0  14441  rmodislmodlem  14659  rmodislmod  14660  cnfldexp  14886  dvdsrzring  14910  znf1o  14958  eltg  15076  eltg2  15077  tgss  15087  tgss2  15103  basgen2  15105  bastop1  15107  opnneiss  15182  cnrest  15259  txss12  15290  hmeofvalg  15327  txswaphmeolem  15344  txswaphmeo  15345  blpnfctr  15463  metequiv  15519  metcnp3  15535  qtopbasss  15545  reopnap  15570  bl2ioo  15574  ioo2bl  15575  ioo2blex  15576  cncfval  15596  divccncfap  15614  addccncf  15624  expcncf  15633  dvexp  15735  dvmptfsum  15749  dvef  15751  efle  15800  reapef  15802  ptolemy  15848  logleb  15899  lgsprme0  16075  gausslemma2dlem1a  16091  gausslemma2dlem4  16097  lgsquadlem3  16112  2lgsoddprmlem2  16139  upgrpredgv  16301  uhgr2edg  16361  issubgr  16412  subgrprop  16414  subuhgr  16427  subupgr  16428  subumgr  16429  subusgr  16430  upgriswlkdc  16515  upgrwlkvtxedg  16519  g0wlk0  16525  clwwlkn1  16573  clwwlknonex2lem2  16593  dichmul0orlem3  16669  uzdcinzz  16740  exmidsbthrlem  16972  triap  16983