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  4148  elnn  4755  soinxp  4847  seinxp  4848  brelrng  5015  dminss  5205  imainss  5206  funsng  5430  funcnvuni  5453  f1co  5613  f1ocnv  5655  fun11iun  5663  funimass4  5756  fndmdifcom  5818  fsn2  5885  fvtp2g  5927  fvtp3g  5928  fvtp2  5930  fvtp3  5931  riotaeqimp  6066  acexmid  6087  oveqan12rd  6108  cofunex2g  6343  brtposg  6529  tposoprab  6555  smores3  6568  smores2  6569  smoel  6575  tfri3  6642  rdgtfr  6649  rdgruledefgg  6650  omcl  6738  oeicl  6739  nnmsucr  6765  nnmcom  6766  nndir  6767  nnaordi  6785  nnaordr  6787  nnaword  6788  nnmordi  6793  nnaordex  6805  nnm00  6807  ersym  6823  elecg  6851  riinerm  6886  ecopovsym  6909  ecopovsymg  6912  ecovcom  6920  ecovicom  6921  mapvalg  6936  pmvalg  6937  elpmg  6942  elmapssres  6958  pmss12g  6960  ixpconstg  6993  domssr  7068  ener  7070  domtr  7076  f1imaeng  7083  fundmen  7098  xpcomco  7128  xpsnen2g  7131  xpdom2  7133  xpdom1g  7135  enen2  7145  domen2  7147  ssfilem  7181  ssfilemd  7183  diffitest  7195  fiintim  7242  fundmfibi  7256  f1setfi  7322  cnvti  7365  djuex  7389  nnnninf  7472  netap  7626  2omotaplemap  7629  ltsopi  7693  pitric  7694  pitri3or  7695  addcompig  7702  mulcompig  7704  ltapig  7711  ltmpig  7712  nnppipi  7716  addcomnqg  7754  addassnqg  7755  distrnqg  7760  recexnq  7763  nqtri3or  7769  ltmnqg  7774  lt2addnq  7777  lt2mulnq  7778  ltbtwnnqq  7788  prarloclemarch2  7792  enq0ref  7806  distrnq0  7832  mulcomnq0  7833  prcdnql  7857  prcunqu  7858  prarloclemlt  7866  genpassl  7897  genpassu  7898  nqprloc  7918  nqpru  7925  appdiv0nq  7937  addcomprg  7951  mulcomprg  7953  distrlem4prl  7957  distrlem4pru  7958  1idprl  7963  1idpru  7964  ltsopr  7969  recexprlemss1l  8008  recexprlemss1u  8009  gt0srpr  8121  mulcomsrg  8130  ltsosr  8137  aptisr  8152  mulextsr1  8154  map2psrprg  8178  axaddcom  8243  axltwlin  8399  axapti  8402  letri3  8412  eqlelt  8418  mul31  8464  cnegexlem3  8510  subval  8525  subcl  8532  pncan2  8540  pncan3  8541  npcan  8542  addsubeq4  8548  npncan3  8571  negsubdi2  8592  muladd  8718  subdi  8719  mulneg2  8730  mulsub  8735  ltleadd  8781  ltsubpos  8789  posdif  8790  addge01  8807  lesub0  8814  reapneg  8933  prodgt02  9191  prodge02  9193  ltdivmul  9214  lerec  9222  lediv2a  9233  le2msq  9239  msq11  9240  lbreu  9283  dfinfre  9294  creur  9297  creui  9298  cju  9299  indval  9305  nnmulcl  9334  nndivtr  9355  avgle1  9557  avgle2  9558  nn0nnaddcl  9605  zletric  9699  zrevaddcl  9706  znnsub  9707  znn0sub  9721  ltsubnn0  9723  zdclt  9733  zextlt  9749  gtndiv  9752  prime  9756  peano5uzti  9765  uztrn2  9956  uztric  9960  uz11  9961  nn0pzuz  10003  indstr  10009  supinfneg  10011  infsupneg  10012  eluzdc  10026  qrevaddcl  10060  difrp  10110  xrltnsym  10212  xrltso  10215  xrlttri3  10216  xrletri3  10223  xleneg  10256  xaddcom  10280  xposdif  10301  ixxssixx  10321  iccid  10344  iooshf  10371  iccsupr  10385  iooneg  10407  iccneg  10408  fztri3or  10460  fzdcel  10461  fzn  10463  fzen  10464  fzass4  10485  fzrev  10508  fznn  10513  elfzp1b  10521  elfzm1b  10522  fz0fzdiffz0  10554  difelfznle  10559  fzon  10591  fzo0n  10592  fzonmapblen  10616  elfzoextl  10626  eluzgtdifelfzo  10632  ubmelm1fzo  10661  subfzo0  10678  qletric  10693  qdclt  10697  qdcle  10698  ioo0  10711  ico0  10713  ioc0  10714  flqbi  10746  flqbi2  10747  flqzadd  10754  modfzo0difsn  10853  fzfig  10888  expcllem  11008  expap0  11027  mulbinom2  11114  expnbnd  11122  sq11ap  11166  hashfacen  11306  iswrdinn0  11331  ccatsymb  11392  ccatalpha  11403  swrd0g  11454  swrdsbslen  11460  swrdspsleq  11461  wrd2ind  11517  pfxccatin12lem1  11522  pfxccatin12lem2  11525  pfxccatin12  11527  swrdccat3blem  11533  shftlem  11603  shftuz  11604  shftfvalg  11605  ovshftex  11606  shftfval  11608  shftval4  11615  shftval5  11616  2shfti  11618  mulreap  11651  sqrt11ap  11826  abs3dif  11894  abs2difabs  11897  maxabslemval  11997  maxle2  12001  maxclpr  12011  2zsupmax  12015  mingeb  12033  2zinfmin  12034  xrmaxiflemval  12041  xrmax2sup  12045  iooinsup  12068  climshftlemg  12093  fsumcnv  12229  explecnv  12297  geo2lim  12308  prodmodc  12370  fprodcnv  12417  demoivre  12565  demoivreALT  12566  nndivides  12589  0dvds  12603  muldvds1  12608  muldvds2  12609  dvdssubr  12631  dvdsadd2b  12632  odd2np1  12665  mulsucdiv2z  12677  ltoddhalfle  12685  ndvdssub  12722  gcdcom  12775  neggcd  12785  gcdabs2  12792  modgcd  12793  bezoutlemaz  12805  dfgcd2  12816  lcmcom  12867  neglcm  12878  lcmgcdeq  12886  coprmdvds  12895  qredeq  12899  divgcdcoprmex  12905  isprm3  12921  prmind2  12923  dvdsprm  12941  cncongrprm  12961  sqrt2irr  12966  nnmaxpw  12978  hashgcdeq  13047  modprmn0modprm0  13064  coprimeprodsq  13065  pythagtriplem1  13073  pythagtriplem4  13076  pc2dvds  13138  pc11  13139  pcz  13140  pcprod  13154  prmunb  13170  1arithlem2  13172  1arithlem3  13173  1arith  13175  ptex  13677  issubmnd  13814  submcl  13845  resmhm2b  13855  grpinvsub  13946  dfgrp3mlem  13962  cntz2ss  14168  cntzrec  14169  imasabl  14230  mgpress  14337  srgmulgass  14400  dfrhm2  14570  isrim0  14577  rmodislmodlem  14796  rmodislmod  14797  cnfldexp  15023  dvdsrzring  15047  znf1o  15095  eltg  15278  eltg2  15279  tgss  15289  tgss2  15305  basgen2  15307  bastop1  15309  opnneiss  15384  cnrest  15461  txss12  15492  hmeofvalg  15529  txswaphmeolem  15546  txswaphmeo  15547  blpnfctr  15665  metequiv  15721  metcnp3  15737  qtopbasss  15747  reopnap  15772  bl2ioo  15776  ioo2bl  15777  ioo2blex  15778  cncfval  15798  divccncfap  15816  addccncf  15826  expcncf  15835  dvexp  15937  dvmptfsum  15951  dvef  15953  efle  16002  reapef  16004  ptolemy  16051  logleb  16105  logdivle  16125  lgsprme0  16366  gausslemma2dlem1a  16382  gausslemma2dlem4  16388  lgsquadlem3  16403  2lgsoddprmlem2  16430  upgrpredgv  16592  uhgr2edg  16652  issubgr  16703  subgrprop  16705  subuhgr  16718  subupgr  16719  subumgr  16720  subusgr  16721  upgriswlkdc  16806  upgrwlkvtxedg  16810  g0wlk0  16816  clwwlkn1  16864  clwwlknonex2lem2  16884  dichmul0orlem3  16960  uzdcinzz  17031  exmidsbthrlem  17273  triap  17284