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  460  anabss4  572  anabsi7  576  anabsi8  577  im2anan9r  594  bi2anan9r  602  syl3anr2  1286  mp3anr1  1329  mp3anr2  1330  mp3anr3  1331  eu5  2066  2exeu  2111  eqeqan12rd  2187  sylan9eqr  2225  r19.29vva  2615  morex  2914  sylan9ssr  3161  riinm  3945  breqan12rd  4006  elnn  4590  soinxp  4681  seinxp  4682  brelrng  4842  dminss  5025  imainss  5026  funsng  5244  funcnvuni  5267  f1co  5415  f1ocnv  5455  fun11iun  5463  funimass4  5547  fndmdifcom  5602  fsn2  5670  fvtp2g  5705  fvtp3g  5706  fvtp2  5708  fvtp3  5709  acexmid  5852  oveqan12rd  5873  cofunex2g  6089  brtposg  6233  tposoprab  6259  smores3  6272  smores2  6273  smoel  6279  tfri3  6346  rdgtfr  6353  rdgruledefgg  6354  omcl  6440  oeicl  6441  nnmsucr  6467  nnmcom  6468  nndir  6469  nnaordi  6487  nnaordr  6489  nnaword  6490  nnmordi  6495  nnaordex  6507  nnm00  6509  ersym  6525  elecg  6551  riinerm  6586  ecopovsym  6609  ecopovsymg  6612  ecovcom  6620  ecovicom  6621  mapvalg  6636  pmvalg  6637  elpmg  6642  elmapssres  6651  pmss12g  6653  ixpconstg  6685  ener  6757  domtr  6763  f1imaeng  6770  fundmen  6784  xpcomco  6804  xpsnen2g  6807  xpdom2  6809  xpdom1g  6811  enen2  6819  domen2  6821  ssfilem  6853  diffitest  6865  fiintim  6906  fundmfibi  6916  cnvti  6996  djuex  7020  nnnninf  7102  ltsopi  7282  pitric  7283  pitri3or  7284  addcompig  7291  mulcompig  7293  ltapig  7300  ltmpig  7301  nnppipi  7305  addcomnqg  7343  addassnqg  7344  distrnqg  7349  recexnq  7352  nqtri3or  7358  ltmnqg  7363  lt2addnq  7366  lt2mulnq  7367  ltbtwnnqq  7377  prarloclemarch2  7381  enq0ref  7395  distrnq0  7421  mulcomnq0  7422  prcdnql  7446  prcunqu  7447  prarloclemlt  7455  genpassl  7486  genpassu  7487  nqprloc  7507  nqpru  7514  appdiv0nq  7526  addcomprg  7540  mulcomprg  7542  distrlem4prl  7546  distrlem4pru  7547  1idprl  7552  1idpru  7553  ltsopr  7558  recexprlemss1l  7597  recexprlemss1u  7598  gt0srpr  7710  mulcomsrg  7719  ltsosr  7726  aptisr  7741  mulextsr1  7743  map2psrprg  7767  axaddcom  7832  axltwlin  7987  axapti  7990  letri3  8000  eqlelt  8006  mul31  8050  cnegexlem3  8096  subval  8111  subcl  8118  pncan2  8126  pncan3  8127  npcan  8128  addsubeq4  8134  npncan3  8157  negsubdi2  8178  muladd  8303  subdi  8304  mulneg2  8315  mulsub  8320  ltleadd  8365  ltsubpos  8373  posdif  8374  addge01  8391  lesub0  8398  reapneg  8516  prodgt02  8769  prodge02  8771  ltdivmul  8792  lerec  8800  lediv2a  8811  le2msq  8817  msq11  8818  lbreu  8861  dfinfre  8872  creur  8875  creui  8876  cju  8877  nnmulcl  8899  nndivtr  8920  avgle1  9118  avgle2  9119  nn0nnaddcl  9166  zletric  9256  zrevaddcl  9262  znnsub  9263  znn0sub  9277  ltsubnn0  9279  zdclt  9289  zextlt  9304  gtndiv  9307  prime  9311  peano5uzti  9320  uztrn2  9504  uztric  9508  uz11  9509  nn0pzuz  9546  indstr  9552  supinfneg  9554  infsupneg  9555  eluzdc  9569  qrevaddcl  9603  difrp  9649  xrltnsym  9750  xrltso  9753  xrlttri3  9754  xrletri3  9761  xleneg  9794  xaddcom  9818  xposdif  9839  ixxssixx  9859  iccid  9882  iooshf  9909  iccsupr  9923  iooneg  9945  iccneg  9946  fztri3or  9995  fzdcel  9996  fzn  9998  fzen  9999  fzass4  10018  fzrev  10040  fznn  10045  elfzp1b  10053  elfzm1b  10054  fz0fzdiffz0  10086  difelfznle  10091  fzon  10122  fzonmapblen  10143  eluzgtdifelfzo  10153  ubmelm1fzo  10182  subfzo0  10198  qletric  10200  ioo0  10216  ico0  10218  ioc0  10219  flqbi  10246  flqbi2  10247  flqzadd  10254  modfzo0difsn  10351  fzfig  10386  expcllem  10487  expap0  10506  mulbinom2  10592  expnbnd  10599  sq11ap  10643  hashfacen  10771  shftlem  10780  shftuz  10781  shftfvalg  10782  ovshftex  10783  shftfval  10785  shftval4  10792  shftval5  10793  2shfti  10795  mulreap  10828  sqrt11ap  11002  abs3dif  11069  abs2difabs  11072  maxabslemval  11172  maxle2  11176  maxclpr  11186  2zsupmax  11189  mingeb  11205  2zinfmin  11206  xrmaxiflemval  11213  xrmax2sup  11217  iooinsup  11240  climshftlemg  11265  fsumcnv  11400  explecnv  11468  geo2lim  11479  prodmodc  11541  fprodcnv  11588  demoivre  11735  demoivreALT  11736  nndivides  11759  0dvds  11773  muldvds1  11778  muldvds2  11779  dvdssubr  11801  dvdsadd2b  11802  odd2np1  11832  mulsucdiv2z  11844  ltoddhalfle  11852  ndvdssub  11889  gcdcom  11928  neggcd  11938  gcdabs2  11945  modgcd  11946  bezoutlemaz  11958  dfgcd2  11969  lcmcom  12018  neglcm  12029  lcmgcdeq  12037  coprmdvds  12046  qredeq  12050  divgcdcoprmex  12056  isprm3  12072  prmind2  12074  dvdsprm  12091  cncongrprm  12111  sqrt2irr  12116  hashgcdeq  12193  modprmn0modprm0  12210  coprimeprodsq  12211  pythagtriplem1  12219  pythagtriplem4  12222  pc2dvds  12283  pc11  12284  pcz  12285  pcprod  12298  prmunb  12314  1arithlem2  12316  1arithlem3  12317  1arith  12319  submcl  12701  eltg  12846  eltg2  12847  tgss  12857  tgss2  12873  basgen2  12875  bastop1  12877  opnneiss  12952  cnrest  13029  txss12  13060  hmeofvalg  13097  txswaphmeolem  13114  txswaphmeo  13115  blpnfctr  13233  metequiv  13289  metcnp3  13305  qtopbasss  13315  reopnap  13332  bl2ioo  13336  ioo2bl  13337  ioo2blex  13338  cncfval  13353  divccncfap  13371  addccncf  13380  expcncf  13386  dvexp  13469  dvef  13482  efle  13491  reapef  13493  ptolemy  13539  logleb  13590  lgsprme0  13737  uzdcinzz  13833  exmidsbthrlem  14054  triap  14061