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  2921  sylan9ssr  3169  riinm  3959  breqan12rd  4020  elnn  4605  soinxp  4696  seinxp  4697  brelrng  4858  dminss  5043  imainss  5044  funsng  5262  funcnvuni  5285  f1co  5433  f1ocnv  5474  fun11iun  5482  funimass4  5566  fndmdifcom  5622  fsn2  5690  fvtp2g  5725  fvtp3g  5726  fvtp2  5728  fvtp3  5729  acexmid  5873  oveqan12rd  5894  cofunex2g  6110  brtposg  6254  tposoprab  6280  smores3  6293  smores2  6294  smoel  6300  tfri3  6367  rdgtfr  6374  rdgruledefgg  6375  omcl  6461  oeicl  6462  nnmsucr  6488  nnmcom  6489  nndir  6490  nnaordi  6508  nnaordr  6510  nnaword  6511  nnmordi  6516  nnaordex  6528  nnm00  6530  ersym  6546  elecg  6572  riinerm  6607  ecopovsym  6630  ecopovsymg  6633  ecovcom  6641  ecovicom  6642  mapvalg  6657  pmvalg  6658  elpmg  6663  elmapssres  6672  pmss12g  6674  ixpconstg  6706  ener  6778  domtr  6784  f1imaeng  6791  fundmen  6805  xpcomco  6825  xpsnen2g  6828  xpdom2  6830  xpdom1g  6832  enen2  6840  domen2  6842  ssfilem  6874  diffitest  6886  fiintim  6927  fundmfibi  6937  cnvti  7017  djuex  7041  nnnninf  7123  netap  7252  2omotaplemap  7255  ltsopi  7318  pitric  7319  pitri3or  7320  addcompig  7327  mulcompig  7329  ltapig  7336  ltmpig  7337  nnppipi  7341  addcomnqg  7379  addassnqg  7380  distrnqg  7385  recexnq  7388  nqtri3or  7394  ltmnqg  7399  lt2addnq  7402  lt2mulnq  7403  ltbtwnnqq  7413  prarloclemarch2  7417  enq0ref  7431  distrnq0  7457  mulcomnq0  7458  prcdnql  7482  prcunqu  7483  prarloclemlt  7491  genpassl  7522  genpassu  7523  nqprloc  7543  nqpru  7550  appdiv0nq  7562  addcomprg  7576  mulcomprg  7578  distrlem4prl  7582  distrlem4pru  7583  1idprl  7588  1idpru  7589  ltsopr  7594  recexprlemss1l  7633  recexprlemss1u  7634  gt0srpr  7746  mulcomsrg  7755  ltsosr  7762  aptisr  7777  mulextsr1  7779  map2psrprg  7803  axaddcom  7868  axltwlin  8024  axapti  8027  letri3  8037  eqlelt  8043  mul31  8087  cnegexlem3  8133  subval  8148  subcl  8155  pncan2  8163  pncan3  8164  npcan  8165  addsubeq4  8171  npncan3  8194  negsubdi2  8215  muladd  8340  subdi  8341  mulneg2  8352  mulsub  8357  ltleadd  8402  ltsubpos  8410  posdif  8411  addge01  8428  lesub0  8435  reapneg  8553  prodgt02  8809  prodge02  8811  ltdivmul  8832  lerec  8840  lediv2a  8851  le2msq  8857  msq11  8858  lbreu  8901  dfinfre  8912  creur  8915  creui  8916  cju  8917  nnmulcl  8939  nndivtr  8960  avgle1  9158  avgle2  9159  nn0nnaddcl  9206  zletric  9296  zrevaddcl  9302  znnsub  9303  znn0sub  9317  ltsubnn0  9319  zdclt  9329  zextlt  9344  gtndiv  9347  prime  9351  peano5uzti  9360  uztrn2  9544  uztric  9548  uz11  9549  nn0pzuz  9586  indstr  9592  supinfneg  9594  infsupneg  9595  eluzdc  9609  qrevaddcl  9643  difrp  9691  xrltnsym  9792  xrltso  9795  xrlttri3  9796  xrletri3  9803  xleneg  9836  xaddcom  9860  xposdif  9881  ixxssixx  9901  iccid  9924  iooshf  9951  iccsupr  9965  iooneg  9987  iccneg  9988  fztri3or  10038  fzdcel  10039  fzn  10041  fzen  10042  fzass4  10061  fzrev  10083  fznn  10088  elfzp1b  10096  elfzm1b  10097  fz0fzdiffz0  10129  difelfznle  10134  fzon  10165  fzonmapblen  10186  eluzgtdifelfzo  10196  ubmelm1fzo  10225  subfzo0  10241  qletric  10243  ioo0  10259  ico0  10261  ioc0  10262  flqbi  10289  flqbi2  10290  flqzadd  10297  modfzo0difsn  10394  fzfig  10429  expcllem  10530  expap0  10549  mulbinom2  10636  expnbnd  10643  sq11ap  10687  hashfacen  10815  shftlem  10824  shftuz  10825  shftfvalg  10826  ovshftex  10827  shftfval  10829  shftval4  10836  shftval5  10837  2shfti  10839  mulreap  10872  sqrt11ap  11046  abs3dif  11113  abs2difabs  11116  maxabslemval  11216  maxle2  11220  maxclpr  11230  2zsupmax  11233  mingeb  11249  2zinfmin  11250  xrmaxiflemval  11257  xrmax2sup  11261  iooinsup  11284  climshftlemg  11309  fsumcnv  11444  explecnv  11512  geo2lim  11523  prodmodc  11585  fprodcnv  11632  demoivre  11779  demoivreALT  11780  nndivides  11803  0dvds  11817  muldvds1  11822  muldvds2  11823  dvdssubr  11845  dvdsadd2b  11846  odd2np1  11877  mulsucdiv2z  11889  ltoddhalfle  11897  ndvdssub  11934  gcdcom  11973  neggcd  11983  gcdabs2  11990  modgcd  11991  bezoutlemaz  12003  dfgcd2  12014  lcmcom  12063  neglcm  12074  lcmgcdeq  12082  coprmdvds  12091  qredeq  12095  divgcdcoprmex  12101  isprm3  12117  prmind2  12119  dvdsprm  12136  cncongrprm  12156  sqrt2irr  12161  hashgcdeq  12238  modprmn0modprm0  12255  coprimeprodsq  12256  pythagtriplem1  12264  pythagtriplem4  12267  pc2dvds  12328  pc11  12329  pcz  12330  pcprod  12343  prmunb  12359  1arithlem2  12361  1arithlem3  12362  1arith  12364  ptex  12712  issubmnd  12842  submcl  12869  grpinvsub  12951  dfgrp3mlem  12967  mgpress  13139  srgmulgass  13170  cnfldexp  13441  dvdsrzring  13463  eltg  13522  eltg2  13523  tgss  13533  tgss2  13549  basgen2  13551  bastop1  13553  opnneiss  13628  cnrest  13705  txss12  13736  hmeofvalg  13773  txswaphmeolem  13790  txswaphmeo  13791  blpnfctr  13909  metequiv  13965  metcnp3  13981  qtopbasss  13991  reopnap  14008  bl2ioo  14012  ioo2bl  14013  ioo2blex  14014  cncfval  14029  divccncfap  14047  addccncf  14056  expcncf  14062  dvexp  14145  dvef  14158  efle  14167  reapef  14169  ptolemy  14215  logleb  14266  lgsprme0  14413  2lgsoddprmlem2  14424  uzdcinzz  14520  exmidsbthrlem  14740  triap  14747