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  1327  mp3anr1  1371  mp3anr2  1372  mp3anr3  1373  stoic1b  1473  cbvaldvaw  1980  eu5  2128  2exeu  2173  eqeqan12rd  2249  sylan9eqr  2287  r19.29vva  2688  morex  3001  sylan9ssr  3252  riinm  4064  breqan12rd  4126  elnn  4728  soinxp  4820  seinxp  4821  brelrng  4988  dminss  5177  imainss  5178  funsng  5402  funcnvuni  5425  f1co  5585  f1ocnv  5627  fun11iun  5635  funimass4  5727  fndmdifcom  5784  fsn2  5851  fvtp2g  5893  fvtp3g  5894  fvtp2  5896  fvtp3  5897  riotaeqimp  6028  acexmid  6049  oveqan12rd  6070  cofunex2g  6303  brtposg  6485  tposoprab  6511  smores3  6524  smores2  6525  smoel  6531  tfri3  6598  rdgtfr  6605  rdgruledefgg  6606  omcl  6694  oeicl  6695  nnmsucr  6721  nnmcom  6722  nndir  6723  nnaordi  6741  nnaordr  6743  nnaword  6744  nnmordi  6749  nnaordex  6761  nnm00  6763  ersym  6779  elecg  6807  riinerm  6842  ecopovsym  6865  ecopovsymg  6868  ecovcom  6876  ecovicom  6877  mapvalg  6892  pmvalg  6893  elpmg  6898  elmapssres  6907  pmss12g  6909  ixpconstg  6942  domssr  7017  ener  7019  domtr  7025  f1imaeng  7032  fundmen  7047  xpcomco  7077  xpsnen2g  7080  xpdom2  7082  xpdom1g  7084  enen2  7094  domen2  7096  ssfilem  7130  ssfilemd  7132  diffitest  7144  fiintim  7191  fundmfibi  7205  cnvti  7310  djuex  7334  nnnninf  7417  netap  7568  2omotaplemap  7571  ltsopi  7635  pitric  7636  pitri3or  7637  addcompig  7644  mulcompig  7646  ltapig  7653  ltmpig  7654  nnppipi  7658  addcomnqg  7696  addassnqg  7697  distrnqg  7702  recexnq  7705  nqtri3or  7711  ltmnqg  7716  lt2addnq  7719  lt2mulnq  7720  ltbtwnnqq  7730  prarloclemarch2  7734  enq0ref  7748  distrnq0  7774  mulcomnq0  7775  prcdnql  7799  prcunqu  7800  prarloclemlt  7808  genpassl  7839  genpassu  7840  nqprloc  7860  nqpru  7867  appdiv0nq  7879  addcomprg  7893  mulcomprg  7895  distrlem4prl  7899  distrlem4pru  7900  1idprl  7905  1idpru  7906  ltsopr  7911  recexprlemss1l  7950  recexprlemss1u  7951  gt0srpr  8063  mulcomsrg  8072  ltsosr  8079  aptisr  8094  mulextsr1  8096  map2psrprg  8120  axaddcom  8185  axltwlin  8341  axapti  8344  letri3  8354  eqlelt  8360  mul31  8404  cnegexlem3  8450  subval  8465  subcl  8472  pncan2  8480  pncan3  8481  npcan  8482  addsubeq4  8488  npncan3  8511  negsubdi2  8532  muladd  8657  subdi  8658  mulneg2  8669  mulsub  8674  ltleadd  8720  ltsubpos  8728  posdif  8729  addge01  8746  lesub0  8753  reapneg  8871  prodgt02  9127  prodge02  9129  ltdivmul  9150  lerec  9158  lediv2a  9169  le2msq  9175  msq11  9176  lbreu  9219  dfinfre  9230  creur  9233  creui  9234  cju  9235  nnmulcl  9258  nndivtr  9279  avgle1  9479  avgle2  9480  nn0nnaddcl  9527  zletric  9621  zrevaddcl  9628  znnsub  9629  znn0sub  9643  ltsubnn0  9645  zdclt  9655  zextlt  9670  gtndiv  9673  prime  9677  peano5uzti  9686  uztrn2  9872  uztric  9876  uz11  9877  nn0pzuz  9919  indstr  9925  supinfneg  9927  infsupneg  9928  eluzdc  9942  qrevaddcl  9976  difrp  10025  xrltnsym  10126  xrltso  10129  xrlttri3  10130  xrletri3  10137  xleneg  10170  xaddcom  10194  xposdif  10215  ixxssixx  10235  iccid  10258  iooshf  10285  iccsupr  10299  iooneg  10321  iccneg  10322  fztri3or  10373  fzdcel  10374  fzn  10376  fzen  10377  fzass4  10396  fzrev  10418  fznn  10423  elfzp1b  10431  elfzm1b  10432  fz0fzdiffz0  10464  difelfznle  10469  fzon  10501  fzo0n  10502  fzonmapblen  10526  elfzoextl  10536  eluzgtdifelfzo  10542  ubmelm1fzo  10571  subfzo0  10588  qletric  10601  qdclt  10605  qdcle  10606  ioo0  10619  ico0  10621  ioc0  10622  flqbi  10650  flqbi2  10651  flqzadd  10658  modfzo0difsn  10757  fzfig  10792  expcllem  10912  expap0  10931  mulbinom2  11018  expnbnd  11025  sq11ap  11069  hashfacen  11208  iswrdinn0  11229  ccatsymb  11290  ccatalpha  11301  swrd0g  11352  swrdsbslen  11358  swrdspsleq  11359  wrd2ind  11415  pfxccatin12lem1  11420  pfxccatin12lem2  11423  pfxccatin12  11425  swrdccat3blem  11431  shftlem  11501  shftuz  11502  shftfvalg  11503  ovshftex  11504  shftfval  11506  shftval4  11513  shftval5  11514  2shfti  11516  mulreap  11549  sqrt11ap  11723  abs3dif  11790  abs2difabs  11793  maxabslemval  11893  maxle2  11897  maxclpr  11907  2zsupmax  11911  mingeb  11927  2zinfmin  11928  xrmaxiflemval  11935  xrmax2sup  11939  iooinsup  11962  climshftlemg  11987  fsumcnv  12123  explecnv  12191  geo2lim  12202  prodmodc  12264  fprodcnv  12311  demoivre  12459  demoivreALT  12460  nndivides  12483  0dvds  12497  muldvds1  12502  muldvds2  12503  dvdssubr  12525  dvdsadd2b  12526  odd2np1  12559  mulsucdiv2z  12571  ltoddhalfle  12579  ndvdssub  12616  gcdcom  12669  neggcd  12679  gcdabs2  12686  modgcd  12687  bezoutlemaz  12699  dfgcd2  12710  lcmcom  12761  neglcm  12772  lcmgcdeq  12780  coprmdvds  12789  qredeq  12793  divgcdcoprmex  12799  isprm3  12815  prmind2  12817  dvdsprm  12834  cncongrprm  12854  sqrt2irr  12859  hashgcdeq  12937  modprmn0modprm0  12954  coprimeprodsq  12955  pythagtriplem1  12963  pythagtriplem4  12966  pc2dvds  13028  pc11  13029  pcz  13030  pcprod  13044  prmunb  13060  1arithlem2  13062  1arithlem3  13063  1arith  13065  ptex  13477  issubmnd  13655  submcl  13692  resmhm2b  13702  grpinvsub  13795  dfgrp3mlem  13811  imasabl  14053  mgpress  14075  srgmulgass  14133  dfrhm2  14299  isrim0  14306  rmodislmodlem  14498  rmodislmod  14499  cnfldexp  14725  dvdsrzring  14751  znf1o  14799  eltg  14917  eltg2  14918  tgss  14928  tgss2  14944  basgen2  14946  bastop1  14948  opnneiss  15023  cnrest  15100  txss12  15131  hmeofvalg  15168  txswaphmeolem  15185  txswaphmeo  15186  blpnfctr  15304  metequiv  15360  metcnp3  15376  qtopbasss  15386  reopnap  15411  bl2ioo  15415  ioo2bl  15416  ioo2blex  15417  cncfval  15437  divccncfap  15455  addccncf  15465  expcncf  15474  dvexp  15576  dvmptfsum  15590  dvef  15592  efle  15641  reapef  15643  ptolemy  15689  logleb  15740  lgsprme0  15915  gausslemma2dlem1a  15931  gausslemma2dlem4  15937  lgsquadlem3  15952  2lgsoddprmlem2  15979  upgrpredgv  16141  uhgr2edg  16201  issubgr  16252  subgrprop  16254  subuhgr  16267  subupgr  16268  subumgr  16269  subusgr  16270  upgriswlkdc  16355  upgrwlkvtxedg  16359  g0wlk0  16365  clwwlkn1  16413  clwwlknonex2lem2  16433  uzdcinzz  16570  exmidsbthrlem  16802  triap  16813