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  599  bi2anan9r  607  syl3anr2  1291  mp3anr1  1334  mp3anr2  1335  mp3anr3  1336  stoic1b  1428  eu5  2073  2exeu  2118  eqeqan12rd  2194  sylan9eqr  2232  r19.29vva  2622  morex  2923  sylan9ssr  3171  riinm  3961  breqan12rd  4022  elnn  4607  soinxp  4698  seinxp  4699  brelrng  4860  dminss  5045  imainss  5046  funsng  5264  funcnvuni  5287  f1co  5435  f1ocnv  5476  fun11iun  5484  funimass4  5569  fndmdifcom  5625  fsn2  5693  fvtp2g  5728  fvtp3g  5729  fvtp2  5731  fvtp3  5732  acexmid  5877  oveqan12rd  5898  cofunex2g  6114  brtposg  6258  tposoprab  6284  smores3  6297  smores2  6298  smoel  6304  tfri3  6371  rdgtfr  6378  rdgruledefgg  6379  omcl  6465  oeicl  6466  nnmsucr  6492  nnmcom  6493  nndir  6494  nnaordi  6512  nnaordr  6514  nnaword  6515  nnmordi  6520  nnaordex  6532  nnm00  6534  ersym  6550  elecg  6576  riinerm  6611  ecopovsym  6634  ecopovsymg  6637  ecovcom  6645  ecovicom  6646  mapvalg  6661  pmvalg  6662  elpmg  6667  elmapssres  6676  pmss12g  6678  ixpconstg  6710  ener  6782  domtr  6788  f1imaeng  6795  fundmen  6809  xpcomco  6829  xpsnen2g  6832  xpdom2  6834  xpdom1g  6836  enen2  6844  domen2  6846  ssfilem  6878  diffitest  6890  fiintim  6931  fundmfibi  6941  cnvti  7021  djuex  7045  nnnninf  7127  netap  7256  2omotaplemap  7259  ltsopi  7322  pitric  7323  pitri3or  7324  addcompig  7331  mulcompig  7333  ltapig  7340  ltmpig  7341  nnppipi  7345  addcomnqg  7383  addassnqg  7384  distrnqg  7389  recexnq  7392  nqtri3or  7398  ltmnqg  7403  lt2addnq  7406  lt2mulnq  7407  ltbtwnnqq  7417  prarloclemarch2  7421  enq0ref  7435  distrnq0  7461  mulcomnq0  7462  prcdnql  7486  prcunqu  7487  prarloclemlt  7495  genpassl  7526  genpassu  7527  nqprloc  7547  nqpru  7554  appdiv0nq  7566  addcomprg  7580  mulcomprg  7582  distrlem4prl  7586  distrlem4pru  7587  1idprl  7592  1idpru  7593  ltsopr  7598  recexprlemss1l  7637  recexprlemss1u  7638  gt0srpr  7750  mulcomsrg  7759  ltsosr  7766  aptisr  7781  mulextsr1  7783  map2psrprg  7807  axaddcom  7872  axltwlin  8028  axapti  8031  letri3  8041  eqlelt  8047  mul31  8091  cnegexlem3  8137  subval  8152  subcl  8159  pncan2  8167  pncan3  8168  npcan  8169  addsubeq4  8175  npncan3  8198  negsubdi2  8219  muladd  8344  subdi  8345  mulneg2  8356  mulsub  8361  ltleadd  8406  ltsubpos  8414  posdif  8415  addge01  8432  lesub0  8439  reapneg  8557  prodgt02  8813  prodge02  8815  ltdivmul  8836  lerec  8844  lediv2a  8855  le2msq  8861  msq11  8862  lbreu  8905  dfinfre  8916  creur  8919  creui  8920  cju  8921  nnmulcl  8943  nndivtr  8964  avgle1  9162  avgle2  9163  nn0nnaddcl  9210  zletric  9300  zrevaddcl  9306  znnsub  9307  znn0sub  9321  ltsubnn0  9323  zdclt  9333  zextlt  9348  gtndiv  9351  prime  9355  peano5uzti  9364  uztrn2  9548  uztric  9552  uz11  9553  nn0pzuz  9590  indstr  9596  supinfneg  9598  infsupneg  9599  eluzdc  9613  qrevaddcl  9647  difrp  9695  xrltnsym  9796  xrltso  9799  xrlttri3  9800  xrletri3  9807  xleneg  9840  xaddcom  9864  xposdif  9885  ixxssixx  9905  iccid  9928  iooshf  9955  iccsupr  9969  iooneg  9991  iccneg  9992  fztri3or  10042  fzdcel  10043  fzn  10045  fzen  10046  fzass4  10065  fzrev  10087  fznn  10092  elfzp1b  10100  elfzm1b  10101  fz0fzdiffz0  10133  difelfznle  10138  fzon  10169  fzonmapblen  10190  eluzgtdifelfzo  10200  ubmelm1fzo  10229  subfzo0  10245  qletric  10247  ioo0  10263  ico0  10265  ioc0  10266  flqbi  10293  flqbi2  10294  flqzadd  10301  modfzo0difsn  10398  fzfig  10433  expcllem  10534  expap0  10553  mulbinom2  10640  expnbnd  10647  sq11ap  10691  hashfacen  10819  shftlem  10828  shftuz  10829  shftfvalg  10830  ovshftex  10831  shftfval  10833  shftval4  10840  shftval5  10841  2shfti  10843  mulreap  10876  sqrt11ap  11050  abs3dif  11117  abs2difabs  11120  maxabslemval  11220  maxle2  11224  maxclpr  11234  2zsupmax  11237  mingeb  11253  2zinfmin  11254  xrmaxiflemval  11261  xrmax2sup  11265  iooinsup  11288  climshftlemg  11313  fsumcnv  11448  explecnv  11516  geo2lim  11527  prodmodc  11589  fprodcnv  11636  demoivre  11783  demoivreALT  11784  nndivides  11807  0dvds  11821  muldvds1  11826  muldvds2  11827  dvdssubr  11849  dvdsadd2b  11850  odd2np1  11881  mulsucdiv2z  11893  ltoddhalfle  11901  ndvdssub  11938  gcdcom  11977  neggcd  11987  gcdabs2  11994  modgcd  11995  bezoutlemaz  12007  dfgcd2  12018  lcmcom  12067  neglcm  12078  lcmgcdeq  12086  coprmdvds  12095  qredeq  12099  divgcdcoprmex  12105  isprm3  12121  prmind2  12123  dvdsprm  12140  cncongrprm  12160  sqrt2irr  12165  hashgcdeq  12242  modprmn0modprm0  12259  coprimeprodsq  12260  pythagtriplem1  12268  pythagtriplem4  12271  pc2dvds  12332  pc11  12333  pcz  12334  pcprod  12347  prmunb  12363  1arithlem2  12365  1arithlem3  12366  1arith  12368  ptex  12719  issubmnd  12849  submcl  12876  grpinvsub  12958  dfgrp3mlem  12974  mgpress  13147  srgmulgass  13178  rmodislmodlem  13446  rmodislmod  13447  cnfldexp  13611  dvdsrzring  13633  eltg  13692  eltg2  13693  tgss  13703  tgss2  13719  basgen2  13721  bastop1  13723  opnneiss  13798  cnrest  13875  txss12  13906  hmeofvalg  13943  txswaphmeolem  13960  txswaphmeo  13961  blpnfctr  14079  metequiv  14135  metcnp3  14151  qtopbasss  14161  reopnap  14178  bl2ioo  14182  ioo2bl  14183  ioo2blex  14184  cncfval  14199  divccncfap  14217  addccncf  14226  expcncf  14232  dvexp  14315  dvef  14328  efle  14337  reapef  14339  ptolemy  14385  logleb  14436  lgsprme0  14583  2lgsoddprmlem2  14594  uzdcinzz  14690  exmidsbthrlem  14911  triap  14918