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  577  anabsi7  581  anabsi8  582  im2anan9r  601  bi2anan9r  609  syl3anr2  1324  mp3anr1  1368  mp3anr2  1369  mp3anr3  1370  stoic1b  1470  cbvaldvaw  1977  eu5  2125  2exeu  2170  eqeqan12rd  2246  sylan9eqr  2284  r19.29vva  2676  morex  2988  sylan9ssr  3239  riinm  4041  breqan12rd  4103  elnn  4702  soinxp  4794  seinxp  4795  brelrng  4961  dminss  5149  imainss  5150  funsng  5373  funcnvuni  5396  f1co  5551  f1ocnv  5593  fun11iun  5601  funimass4  5692  fndmdifcom  5749  fsn2  5817  fvtp2g  5858  fvtp3g  5859  fvtp2  5861  fvtp3  5862  riotaeqimp  5991  acexmid  6012  oveqan12rd  6033  cofunex2g  6267  brtposg  6415  tposoprab  6441  smores3  6454  smores2  6455  smoel  6461  tfri3  6528  rdgtfr  6535  rdgruledefgg  6536  omcl  6624  oeicl  6625  nnmsucr  6651  nnmcom  6652  nndir  6653  nnaordi  6671  nnaordr  6673  nnaword  6674  nnmordi  6679  nnaordex  6691  nnm00  6693  ersym  6709  elecg  6737  riinerm  6772  ecopovsym  6795  ecopovsymg  6798  ecovcom  6806  ecovicom  6807  mapvalg  6822  pmvalg  6823  elpmg  6828  elmapssres  6837  pmss12g  6839  ixpconstg  6871  domssr  6946  ener  6948  domtr  6954  f1imaeng  6961  fundmen  6976  xpcomco  7005  xpsnen2g  7008  xpdom2  7010  xpdom1g  7012  enen2  7022  domen2  7024  ssfilem  7057  diffitest  7069  fiintim  7116  fundmfibi  7128  cnvti  7209  djuex  7233  nnnninf  7316  netap  7463  2omotaplemap  7466  ltsopi  7530  pitric  7531  pitri3or  7532  addcompig  7539  mulcompig  7541  ltapig  7548  ltmpig  7549  nnppipi  7553  addcomnqg  7591  addassnqg  7592  distrnqg  7597  recexnq  7600  nqtri3or  7606  ltmnqg  7611  lt2addnq  7614  lt2mulnq  7615  ltbtwnnqq  7625  prarloclemarch2  7629  enq0ref  7643  distrnq0  7669  mulcomnq0  7670  prcdnql  7694  prcunqu  7695  prarloclemlt  7703  genpassl  7734  genpassu  7735  nqprloc  7755  nqpru  7762  appdiv0nq  7774  addcomprg  7788  mulcomprg  7790  distrlem4prl  7794  distrlem4pru  7795  1idprl  7800  1idpru  7801  ltsopr  7806  recexprlemss1l  7845  recexprlemss1u  7846  gt0srpr  7958  mulcomsrg  7967  ltsosr  7974  aptisr  7989  mulextsr1  7991  map2psrprg  8015  axaddcom  8080  axltwlin  8237  axapti  8240  letri3  8250  eqlelt  8256  mul31  8300  cnegexlem3  8346  subval  8361  subcl  8368  pncan2  8376  pncan3  8377  npcan  8378  addsubeq4  8384  npncan3  8407  negsubdi2  8428  muladd  8553  subdi  8554  mulneg2  8565  mulsub  8570  ltleadd  8616  ltsubpos  8624  posdif  8625  addge01  8642  lesub0  8649  reapneg  8767  prodgt02  9023  prodge02  9025  ltdivmul  9046  lerec  9054  lediv2a  9065  le2msq  9071  msq11  9072  lbreu  9115  dfinfre  9126  creur  9129  creui  9130  cju  9131  nnmulcl  9154  nndivtr  9175  avgle1  9375  avgle2  9376  nn0nnaddcl  9423  zletric  9513  zrevaddcl  9520  znnsub  9521  znn0sub  9535  ltsubnn0  9537  zdclt  9547  zextlt  9562  gtndiv  9565  prime  9569  peano5uzti  9578  uztrn2  9764  uztric  9768  uz11  9769  nn0pzuz  9811  indstr  9817  supinfneg  9819  infsupneg  9820  eluzdc  9834  qrevaddcl  9868  difrp  9917  xrltnsym  10018  xrltso  10021  xrlttri3  10022  xrletri3  10029  xleneg  10062  xaddcom  10086  xposdif  10107  ixxssixx  10127  iccid  10150  iooshf  10177  iccsupr  10191  iooneg  10213  iccneg  10214  fztri3or  10264  fzdcel  10265  fzn  10267  fzen  10268  fzass4  10287  fzrev  10309  fznn  10314  elfzp1b  10322  elfzm1b  10323  fz0fzdiffz0  10355  difelfznle  10360  fzon  10392  fzo0n  10393  fzonmapblen  10416  elfzoextl  10426  eluzgtdifelfzo  10432  ubmelm1fzo  10461  subfzo0  10478  qletric  10491  qdclt  10495  qdcle  10496  ioo0  10509  ico0  10511  ioc0  10512  flqbi  10540  flqbi2  10541  flqzadd  10548  modfzo0difsn  10647  fzfig  10682  expcllem  10802  expap0  10821  mulbinom2  10908  expnbnd  10915  sq11ap  10959  hashfacen  11090  iswrdinn0  11108  ccatsymb  11169  ccatalpha  11180  swrd0g  11231  swrdsbslen  11237  swrdspsleq  11238  wrd2ind  11294  pfxccatin12lem1  11299  pfxccatin12lem2  11302  pfxccatin12  11304  swrdccat3blem  11310  shftlem  11367  shftuz  11368  shftfvalg  11369  ovshftex  11370  shftfval  11372  shftval4  11379  shftval5  11380  2shfti  11382  mulreap  11415  sqrt11ap  11589  abs3dif  11656  abs2difabs  11659  maxabslemval  11759  maxle2  11763  maxclpr  11773  2zsupmax  11777  mingeb  11793  2zinfmin  11794  xrmaxiflemval  11801  xrmax2sup  11805  iooinsup  11828  climshftlemg  11853  fsumcnv  11988  explecnv  12056  geo2lim  12067  prodmodc  12129  fprodcnv  12176  demoivre  12324  demoivreALT  12325  nndivides  12348  0dvds  12362  muldvds1  12367  muldvds2  12368  dvdssubr  12390  dvdsadd2b  12391  odd2np1  12424  mulsucdiv2z  12436  ltoddhalfle  12444  ndvdssub  12481  gcdcom  12534  neggcd  12544  gcdabs2  12551  modgcd  12552  bezoutlemaz  12564  dfgcd2  12575  lcmcom  12626  neglcm  12637  lcmgcdeq  12645  coprmdvds  12654  qredeq  12658  divgcdcoprmex  12664  isprm3  12680  prmind2  12682  dvdsprm  12699  cncongrprm  12719  sqrt2irr  12724  hashgcdeq  12802  modprmn0modprm0  12819  coprimeprodsq  12820  pythagtriplem1  12828  pythagtriplem4  12831  pc2dvds  12893  pc11  12894  pcz  12895  pcprod  12909  prmunb  12925  1arithlem2  12927  1arithlem3  12928  1arith  12930  ptex  13337  issubmnd  13515  submcl  13552  resmhm2b  13562  grpinvsub  13655  dfgrp3mlem  13671  imasabl  13913  mgpress  13934  srgmulgass  13992  dfrhm2  14158  isrim0  14165  rmodislmodlem  14354  rmodislmod  14355  cnfldexp  14581  dvdsrzring  14607  znf1o  14655  eltg  14766  eltg2  14767  tgss  14777  tgss2  14793  basgen2  14795  bastop1  14797  opnneiss  14872  cnrest  14949  txss12  14980  hmeofvalg  15017  txswaphmeolem  15034  txswaphmeo  15035  blpnfctr  15153  metequiv  15209  metcnp3  15225  qtopbasss  15235  reopnap  15260  bl2ioo  15264  ioo2bl  15265  ioo2blex  15266  cncfval  15286  divccncfap  15304  addccncf  15314  expcncf  15323  dvexp  15425  dvmptfsum  15439  dvef  15441  efle  15490  reapef  15492  ptolemy  15538  logleb  15589  lgsprme0  15761  gausslemma2dlem1a  15777  gausslemma2dlem4  15783  lgsquadlem3  15798  2lgsoddprmlem2  15825  upgrpredgv  15985  uhgr2edg  16045  upgriswlkdc  16157  upgrwlkvtxedg  16161  g0wlk0  16167  clwwlkn1  16213  clwwlknonex2lem2  16233  uzdcinzz  16330  exmidsbthrlem  16562  triap  16569