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  1326  mp3anr1  1370  mp3anr2  1371  mp3anr3  1372  stoic1b  1472  cbvaldvaw  1979  eu5  2127  2exeu  2172  eqeqan12rd  2248  sylan9eqr  2286  r19.29vva  2678  morex  2990  sylan9ssr  3241  riinm  4043  breqan12rd  4105  elnn  4704  soinxp  4796  seinxp  4797  brelrng  4963  dminss  5151  imainss  5152  funsng  5376  funcnvuni  5399  f1co  5554  f1ocnv  5596  fun11iun  5604  funimass4  5696  fndmdifcom  5753  fsn2  5821  fvtp2g  5862  fvtp3g  5863  fvtp2  5865  fvtp3  5866  riotaeqimp  5995  acexmid  6016  oveqan12rd  6037  cofunex2g  6271  brtposg  6419  tposoprab  6445  smores3  6458  smores2  6459  smoel  6465  tfri3  6532  rdgtfr  6539  rdgruledefgg  6540  omcl  6628  oeicl  6629  nnmsucr  6655  nnmcom  6656  nndir  6657  nnaordi  6675  nnaordr  6677  nnaword  6678  nnmordi  6683  nnaordex  6695  nnm00  6697  ersym  6713  elecg  6741  riinerm  6776  ecopovsym  6799  ecopovsymg  6802  ecovcom  6810  ecovicom  6811  mapvalg  6826  pmvalg  6827  elpmg  6832  elmapssres  6841  pmss12g  6843  ixpconstg  6875  domssr  6950  ener  6952  domtr  6958  f1imaeng  6965  fundmen  6980  xpcomco  7009  xpsnen2g  7012  xpdom2  7014  xpdom1g  7016  enen2  7026  domen2  7028  ssfilem  7061  ssfilemd  7063  diffitest  7075  fiintim  7122  fundmfibi  7136  cnvti  7217  djuex  7241  nnnninf  7324  netap  7472  2omotaplemap  7475  ltsopi  7539  pitric  7540  pitri3or  7541  addcompig  7548  mulcompig  7550  ltapig  7557  ltmpig  7558  nnppipi  7562  addcomnqg  7600  addassnqg  7601  distrnqg  7606  recexnq  7609  nqtri3or  7615  ltmnqg  7620  lt2addnq  7623  lt2mulnq  7624  ltbtwnnqq  7634  prarloclemarch2  7638  enq0ref  7652  distrnq0  7678  mulcomnq0  7679  prcdnql  7703  prcunqu  7704  prarloclemlt  7712  genpassl  7743  genpassu  7744  nqprloc  7764  nqpru  7771  appdiv0nq  7783  addcomprg  7797  mulcomprg  7799  distrlem4prl  7803  distrlem4pru  7804  1idprl  7809  1idpru  7810  ltsopr  7815  recexprlemss1l  7854  recexprlemss1u  7855  gt0srpr  7967  mulcomsrg  7976  ltsosr  7983  aptisr  7998  mulextsr1  8000  map2psrprg  8024  axaddcom  8089  axltwlin  8246  axapti  8249  letri3  8259  eqlelt  8265  mul31  8309  cnegexlem3  8355  subval  8370  subcl  8377  pncan2  8385  pncan3  8386  npcan  8387  addsubeq4  8393  npncan3  8416  negsubdi2  8437  muladd  8562  subdi  8563  mulneg2  8574  mulsub  8579  ltleadd  8625  ltsubpos  8633  posdif  8634  addge01  8651  lesub0  8658  reapneg  8776  prodgt02  9032  prodge02  9034  ltdivmul  9055  lerec  9063  lediv2a  9074  le2msq  9080  msq11  9081  lbreu  9124  dfinfre  9135  creur  9138  creui  9139  cju  9140  nnmulcl  9163  nndivtr  9184  avgle1  9384  avgle2  9385  nn0nnaddcl  9432  zletric  9522  zrevaddcl  9529  znnsub  9530  znn0sub  9544  ltsubnn0  9546  zdclt  9556  zextlt  9571  gtndiv  9574  prime  9578  peano5uzti  9587  uztrn2  9773  uztric  9777  uz11  9778  nn0pzuz  9820  indstr  9826  supinfneg  9828  infsupneg  9829  eluzdc  9843  qrevaddcl  9877  difrp  9926  xrltnsym  10027  xrltso  10030  xrlttri3  10031  xrletri3  10038  xleneg  10071  xaddcom  10095  xposdif  10116  ixxssixx  10136  iccid  10159  iooshf  10186  iccsupr  10200  iooneg  10222  iccneg  10223  fztri3or  10273  fzdcel  10274  fzn  10276  fzen  10277  fzass4  10296  fzrev  10318  fznn  10323  elfzp1b  10331  elfzm1b  10332  fz0fzdiffz0  10364  difelfznle  10369  fzon  10401  fzo0n  10402  fzonmapblen  10425  elfzoextl  10435  eluzgtdifelfzo  10441  ubmelm1fzo  10470  subfzo0  10487  qletric  10500  qdclt  10504  qdcle  10505  ioo0  10518  ico0  10520  ioc0  10521  flqbi  10549  flqbi2  10550  flqzadd  10557  modfzo0difsn  10656  fzfig  10691  expcllem  10811  expap0  10830  mulbinom2  10917  expnbnd  10924  sq11ap  10968  hashfacen  11099  iswrdinn0  11117  ccatsymb  11178  ccatalpha  11189  swrd0g  11240  swrdsbslen  11246  swrdspsleq  11247  wrd2ind  11303  pfxccatin12lem1  11308  pfxccatin12lem2  11311  pfxccatin12  11313  swrdccat3blem  11319  shftlem  11376  shftuz  11377  shftfvalg  11378  ovshftex  11379  shftfval  11381  shftval4  11388  shftval5  11389  2shfti  11391  mulreap  11424  sqrt11ap  11598  abs3dif  11665  abs2difabs  11668  maxabslemval  11768  maxle2  11772  maxclpr  11782  2zsupmax  11786  mingeb  11802  2zinfmin  11803  xrmaxiflemval  11810  xrmax2sup  11814  iooinsup  11837  climshftlemg  11862  fsumcnv  11997  explecnv  12065  geo2lim  12076  prodmodc  12138  fprodcnv  12185  demoivre  12333  demoivreALT  12334  nndivides  12357  0dvds  12371  muldvds1  12376  muldvds2  12377  dvdssubr  12399  dvdsadd2b  12400  odd2np1  12433  mulsucdiv2z  12445  ltoddhalfle  12453  ndvdssub  12490  gcdcom  12543  neggcd  12553  gcdabs2  12560  modgcd  12561  bezoutlemaz  12573  dfgcd2  12584  lcmcom  12635  neglcm  12646  lcmgcdeq  12654  coprmdvds  12663  qredeq  12667  divgcdcoprmex  12673  isprm3  12689  prmind2  12691  dvdsprm  12708  cncongrprm  12728  sqrt2irr  12733  hashgcdeq  12811  modprmn0modprm0  12828  coprimeprodsq  12829  pythagtriplem1  12837  pythagtriplem4  12840  pc2dvds  12902  pc11  12903  pcz  12904  pcprod  12918  prmunb  12934  1arithlem2  12936  1arithlem3  12937  1arith  12939  ptex  13346  issubmnd  13524  submcl  13561  resmhm2b  13571  grpinvsub  13664  dfgrp3mlem  13680  imasabl  13922  mgpress  13943  srgmulgass  14001  dfrhm2  14167  isrim0  14174  rmodislmodlem  14363  rmodislmod  14364  cnfldexp  14590  dvdsrzring  14616  znf1o  14664  eltg  14775  eltg2  14776  tgss  14786  tgss2  14802  basgen2  14804  bastop1  14806  opnneiss  14881  cnrest  14958  txss12  14989  hmeofvalg  15026  txswaphmeolem  15043  txswaphmeo  15044  blpnfctr  15162  metequiv  15218  metcnp3  15234  qtopbasss  15244  reopnap  15269  bl2ioo  15273  ioo2bl  15274  ioo2blex  15275  cncfval  15295  divccncfap  15313  addccncf  15323  expcncf  15332  dvexp  15434  dvmptfsum  15448  dvef  15450  efle  15499  reapef  15501  ptolemy  15547  logleb  15598  lgsprme0  15770  gausslemma2dlem1a  15786  gausslemma2dlem4  15792  lgsquadlem3  15807  2lgsoddprmlem2  15834  upgrpredgv  15996  uhgr2edg  16056  issubgr  16107  subgrprop  16109  subuhgr  16122  subupgr  16123  subumgr  16124  subusgr  16125  upgriswlkdc  16210  upgrwlkvtxedg  16214  g0wlk0  16220  clwwlkn1  16268  clwwlknonex2lem2  16288  uzdcinzz  16394  exmidsbthrlem  16626  triap  16633