Theorem ancoms 266

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 115	. 2 |- ( ps -> ( ph -> ch ) )
3	2	imp 123	1 |- ( ( ps /\ ph ) -> ch )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  adantl  275  syl2anr  288  anim12ci  337  sylan9bbr  459  anabss4  567  anabsi7  571  anabsi8  572  im2anan9r  589  bi2anan9r  597  syl3anr2  1270  mp3anr1  1313  mp3anr2  1314  mp3anr3  1315  eu5  2047  2exeu  2092  eqeqan12rd  2157  sylan9eqr  2195  r19.29vva  2580  morex  2872  sylan9ssr  3116  riinm  3893  breqan12rd  3954  elnn  4527  soinxp  4617  seinxp  4618  brelrng  4778  dminss  4961  imainss  4962  funsng  5177  funcnvuni  5200  f1co  5348  f1ocnv  5388  fun11iun  5396  funimass4  5480  fndmdifcom  5534  fsn2  5602  fvtp2g  5637  fvtp3g  5638  fvtp2  5640  fvtp3  5641  acexmid  5781  oveqan12rd  5802  cofunex2g  6018  brtposg  6159  tposoprab  6185  smores3  6198  smores2  6199  smoel  6205  tfri3  6272  rdgtfr  6279  rdgruledefgg  6280  omcl  6365  oeicl  6366  nnmsucr  6392  nnmcom  6393  nndir  6394  nnaordi  6412  nnaordr  6414  nnaword  6415  nnmordi  6420  nnaordex  6431  nnm00  6433  ersym  6449  elecg  6475  riinerm  6510  ecopovsym  6533  ecopovsymg  6536  ecovcom  6544  ecovicom  6545  mapvalg  6560  pmvalg  6561  elpmg  6566  elmapssres  6575  pmss12g  6577  ixpconstg  6609  ener  6681  domtr  6687  f1imaeng  6694  fundmen  6708  xpcomco  6728  xpsnen2g  6731  xpdom2  6733  xpdom1g  6735  enen2  6743  domen2  6745  ssfilem  6777  diffitest  6789  fiintim  6825  fundmfibi  6835  cnvti  6914  djuex  6936  nnnninf  7031  ltsopi  7152  pitric  7153  pitri3or  7154  addcompig  7161  mulcompig  7163  ltapig  7170  ltmpig  7171  nnppipi  7175  addcomnqg  7213  addassnqg  7214  distrnqg  7219  recexnq  7222  nqtri3or  7228  ltmnqg  7233  lt2addnq  7236  lt2mulnq  7237  ltbtwnnqq  7247  prarloclemarch2  7251  enq0ref  7265  distrnq0  7291  mulcomnq0  7292  prcdnql  7316  prcunqu  7317  prarloclemlt  7325  genpassl  7356  genpassu  7357  nqprloc  7377  nqpru  7384  appdiv0nq  7396  addcomprg  7410  mulcomprg  7412  distrlem4prl  7416  distrlem4pru  7417  1idprl  7422  1idpru  7423  ltsopr  7428  recexprlemss1l  7467  recexprlemss1u  7468  gt0srpr  7580  mulcomsrg  7589  ltsosr  7596  aptisr  7611  mulextsr1  7613  map2psrprg  7637  axaddcom  7702  axltwlin  7856  axapti  7859  letri3  7869  mul31  7917  cnegexlem3  7963  subval  7978  subcl  7985  pncan2  7993  pncan3  7994  npcan  7995  addsubeq4  8001  npncan3  8024  negsubdi2  8045  muladd  8170  subdi  8171  mulneg2  8182  mulsub  8187  ltleadd  8232  ltsubpos  8240  posdif  8241  addge01  8258  lesub0  8265  reapneg  8383  prodgt02  8635  prodge02  8637  ltdivmul  8658  lerec  8666  lediv2a  8677  le2msq  8683  msq11  8684  lbreu  8727  dfinfre  8738  creur  8741  creui  8742  cju  8743  nnmulcl  8765  nndivtr  8786  avgle1  8984  avgle2  8985  nn0nnaddcl  9032  zletric  9122  zrevaddcl  9128  znnsub  9129  znn0sub  9143  zdclt  9152  zextlt  9167  gtndiv  9170  prime  9174  peano5uzti  9183  uztrn2  9367  uztric  9371  uz11  9372  nn0pzuz  9409  indstr  9415  supinfneg  9417  infsupneg  9418  eluzdc  9431  qrevaddcl  9463  difrp  9509  xrltnsym  9609  xrltso  9612  xrlttri3  9613  xrletri3  9618  xleneg  9650  xaddcom  9674  xposdif  9695  ixxssixx  9715  iccid  9738  iooshf  9765  iccsupr  9779  iooneg  9801  iccneg  9802  fztri3or  9850  fzdcel  9851  fzn  9853  fzen  9854  fzass4  9873  fzrev  9895  fznn  9900  elfzp1b  9908  elfzm1b  9909  fz0fzdiffz0  9938  difelfznle  9943  fzon  9974  fzonmapblen  9995  eluzgtdifelfzo  10005  ubmelm1fzo  10034  subfzo0  10050  qletric  10052  ioo0  10068  ico0  10070  ioc0  10071  flqbi  10094  flqbi2  10095  flqzadd  10102  modfzo0difsn  10199  fzfig  10234  expcllem  10335  expap0  10354  mulbinom2  10439  expnbnd  10446  sq11ap  10489  hashfacen  10611  shftlem  10620  shftuz  10621  shftfvalg  10622  ovshftex  10623  shftfval  10625  shftval4  10632  shftval5  10633  2shfti  10635  mulreap  10668  sqrt11ap  10842  abs3dif  10909  abs2difabs  10912  maxabslemval  11012  maxle2  11016  maxclpr  11026  2zsupmax  11029  xrmaxiflemval  11051  xrmax2sup  11055  iooinsup  11078  climshftlemg  11103  fsumcnv  11238  explecnv  11306  geo2lim  11317  prodmodc  11379  demoivre  11515  demoivreALT  11516  nndivides  11536  0dvds  11549  muldvds1  11554  muldvds2  11555  dvdssubr  11575  dvdsadd2b  11576  odd2np1  11606  mulsucdiv2z  11618  ltoddhalfle  11626  ndvdssub  11663  gcdcom  11698  neggcd  11707  gcdabs2  11714  modgcd  11715  bezoutlemaz  11727  dfgcd2  11738  lcmcom  11781  neglcm  11792  lcmgcdeq  11800  coprmdvds  11809  qredeq  11813  divgcdcoprmex  11819  isprm3  11835  prmind2  11837  dvdsprm  11853  cncongrprm  11871  sqrt2irr  11876  hashgcdeq  11940  eltg  12260  eltg2  12261  tgss  12271  tgss2  12287  basgen2  12289  bastop1  12291  opnneiss  12366  cnrest  12443  txss12  12474  hmeofvalg  12511  txswaphmeolem  12528  txswaphmeo  12529  blpnfctr  12647  metequiv  12703  metcnp3  12719  qtopbasss  12729  reopnap  12746  bl2ioo  12750  ioo2bl  12751  ioo2blex  12752  cncfval  12767  divccncfap  12785  addccncf  12794  expcncf  12800  dvexp  12883  dvef  12896  efle  12905  reapef  12907  ptolemy  12953  logleb  13004  uzdcinzz  13176  exmidsbthrlem  13392  triap  13399