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  2987  sylan9ssr  3238  riinm  4038  breqan12rd  4100  elnn  4698  soinxp  4789  seinxp  4790  brelrng  4955  dminss  5143  imainss  5144  funsng  5367  funcnvuni  5390  f1co  5545  f1ocnv  5587  fun11iun  5595  funimass4  5686  fndmdifcom  5743  fsn2  5811  fvtp2g  5852  fvtp3g  5853  fvtp2  5855  fvtp3  5856  riotaeqimp  5985  acexmid  6006  oveqan12rd  6027  cofunex2g  6261  brtposg  6406  tposoprab  6432  smores3  6445  smores2  6446  smoel  6452  tfri3  6519  rdgtfr  6526  rdgruledefgg  6527  omcl  6615  oeicl  6616  nnmsucr  6642  nnmcom  6643  nndir  6644  nnaordi  6662  nnaordr  6664  nnaword  6665  nnmordi  6670  nnaordex  6682  nnm00  6684  ersym  6700  elecg  6728  riinerm  6763  ecopovsym  6786  ecopovsymg  6789  ecovcom  6797  ecovicom  6798  mapvalg  6813  pmvalg  6814  elpmg  6819  elmapssres  6828  pmss12g  6830  ixpconstg  6862  domssr  6937  ener  6939  domtr  6945  f1imaeng  6952  fundmen  6967  xpcomco  6993  xpsnen2g  6996  xpdom2  6998  xpdom1g  7000  enen2  7010  domen2  7012  ssfilem  7045  diffitest  7057  fiintim  7104  fundmfibi  7116  cnvti  7197  djuex  7221  nnnninf  7304  netap  7451  2omotaplemap  7454  ltsopi  7518  pitric  7519  pitri3or  7520  addcompig  7527  mulcompig  7529  ltapig  7536  ltmpig  7537  nnppipi  7541  addcomnqg  7579  addassnqg  7580  distrnqg  7585  recexnq  7588  nqtri3or  7594  ltmnqg  7599  lt2addnq  7602  lt2mulnq  7603  ltbtwnnqq  7613  prarloclemarch2  7617  enq0ref  7631  distrnq0  7657  mulcomnq0  7658  prcdnql  7682  prcunqu  7683  prarloclemlt  7691  genpassl  7722  genpassu  7723  nqprloc  7743  nqpru  7750  appdiv0nq  7762  addcomprg  7776  mulcomprg  7778  distrlem4prl  7782  distrlem4pru  7783  1idprl  7788  1idpru  7789  ltsopr  7794  recexprlemss1l  7833  recexprlemss1u  7834  gt0srpr  7946  mulcomsrg  7955  ltsosr  7962  aptisr  7977  mulextsr1  7979  map2psrprg  8003  axaddcom  8068  axltwlin  8225  axapti  8228  letri3  8238  eqlelt  8244  mul31  8288  cnegexlem3  8334  subval  8349  subcl  8356  pncan2  8364  pncan3  8365  npcan  8366  addsubeq4  8372  npncan3  8395  negsubdi2  8416  muladd  8541  subdi  8542  mulneg2  8553  mulsub  8558  ltleadd  8604  ltsubpos  8612  posdif  8613  addge01  8630  lesub0  8637  reapneg  8755  prodgt02  9011  prodge02  9013  ltdivmul  9034  lerec  9042  lediv2a  9053  le2msq  9059  msq11  9060  lbreu  9103  dfinfre  9114  creur  9117  creui  9118  cju  9119  nnmulcl  9142  nndivtr  9163  avgle1  9363  avgle2  9364  nn0nnaddcl  9411  zletric  9501  zrevaddcl  9508  znnsub  9509  znn0sub  9523  ltsubnn0  9525  zdclt  9535  zextlt  9550  gtndiv  9553  prime  9557  peano5uzti  9566  uztrn2  9752  uztric  9756  uz11  9757  nn0pzuz  9794  indstr  9800  supinfneg  9802  infsupneg  9803  eluzdc  9817  qrevaddcl  9851  difrp  9900  xrltnsym  10001  xrltso  10004  xrlttri3  10005  xrletri3  10012  xleneg  10045  xaddcom  10069  xposdif  10090  ixxssixx  10110  iccid  10133  iooshf  10160  iccsupr  10174  iooneg  10196  iccneg  10197  fztri3or  10247  fzdcel  10248  fzn  10250  fzen  10251  fzass4  10270  fzrev  10292  fznn  10297  elfzp1b  10305  elfzm1b  10306  fz0fzdiffz0  10338  difelfznle  10343  fzon  10375  fzo0n  10376  fzonmapblen  10399  elfzoextl  10409  eluzgtdifelfzo  10415  ubmelm1fzo  10444  subfzo0  10460  qletric  10473  qdclt  10477  qdcle  10478  ioo0  10491  ico0  10493  ioc0  10494  flqbi  10522  flqbi2  10523  flqzadd  10530  modfzo0difsn  10629  fzfig  10664  expcllem  10784  expap0  10803  mulbinom2  10890  expnbnd  10897  sq11ap  10941  hashfacen  11071  iswrdinn0  11089  ccatsymb  11150  ccatalpha  11161  swrd0g  11207  swrdsbslen  11213  swrdspsleq  11214  wrd2ind  11270  pfxccatin12lem1  11275  pfxccatin12lem2  11278  pfxccatin12  11280  swrdccat3blem  11286  shftlem  11342  shftuz  11343  shftfvalg  11344  ovshftex  11345  shftfval  11347  shftval4  11354  shftval5  11355  2shfti  11357  mulreap  11390  sqrt11ap  11564  abs3dif  11631  abs2difabs  11634  maxabslemval  11734  maxle2  11738  maxclpr  11748  2zsupmax  11752  mingeb  11768  2zinfmin  11769  xrmaxiflemval  11776  xrmax2sup  11780  iooinsup  11803  climshftlemg  11828  fsumcnv  11963  explecnv  12031  geo2lim  12042  prodmodc  12104  fprodcnv  12151  demoivre  12299  demoivreALT  12300  nndivides  12323  0dvds  12337  muldvds1  12342  muldvds2  12343  dvdssubr  12365  dvdsadd2b  12366  odd2np1  12399  mulsucdiv2z  12411  ltoddhalfle  12419  ndvdssub  12456  gcdcom  12509  neggcd  12519  gcdabs2  12526  modgcd  12527  bezoutlemaz  12539  dfgcd2  12550  lcmcom  12601  neglcm  12612  lcmgcdeq  12620  coprmdvds  12629  qredeq  12633  divgcdcoprmex  12639  isprm3  12655  prmind2  12657  dvdsprm  12674  cncongrprm  12694  sqrt2irr  12699  hashgcdeq  12777  modprmn0modprm0  12794  coprimeprodsq  12795  pythagtriplem1  12803  pythagtriplem4  12806  pc2dvds  12868  pc11  12869  pcz  12870  pcprod  12884  prmunb  12900  1arithlem2  12902  1arithlem3  12903  1arith  12905  ptex  13312  issubmnd  13490  submcl  13527  resmhm2b  13537  grpinvsub  13630  dfgrp3mlem  13646  imasabl  13888  mgpress  13909  srgmulgass  13967  dfrhm2  14133  isrim0  14140  rmodislmodlem  14329  rmodislmod  14330  cnfldexp  14556  dvdsrzring  14582  znf1o  14630  eltg  14741  eltg2  14742  tgss  14752  tgss2  14768  basgen2  14770  bastop1  14772  opnneiss  14847  cnrest  14924  txss12  14955  hmeofvalg  14992  txswaphmeolem  15009  txswaphmeo  15010  blpnfctr  15128  metequiv  15184  metcnp3  15200  qtopbasss  15210  reopnap  15235  bl2ioo  15239  ioo2bl  15240  ioo2blex  15241  cncfval  15261  divccncfap  15279  addccncf  15289  expcncf  15298  dvexp  15400  dvmptfsum  15414  dvef  15416  efle  15465  reapef  15467  ptolemy  15513  logleb  15564  lgsprme0  15736  gausslemma2dlem1a  15752  gausslemma2dlem4  15758  lgsquadlem3  15773  2lgsoddprmlem2  15800  upgrpredgv  15959  uhgr2edg  16019  upgriswlkdc  16101  upgrwlkvtxedg  16105  g0wlk0  16111  uzdcinzz  16217  exmidsbthrlem  16450  triap  16457