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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  adantl  277  syl2anr  290  anim12ci  339  sylan9bbr  467  anabss4  583  anabsi7  587  anabsi8  588  im2anan9r  607  bi2anan9r  615  syl3anr2  1331  mp3anr1  1375  mp3anr2  1376  mp3anr3  1377  stoic1b  1477  cbvaldvaw  1986  eu5  2134  2exeu  2179  eqeqan12rd  2255  sylan9eqr  2293  r19.29vva  2696  morex  3010  sylan9ssr  3262  riinm  4085  breqan12rd  4147  elnn  4753  soinxp  4845  seinxp  4846  brelrng  5013  dminss  5202  imainss  5203  funsng  5427  funcnvuni  5450  f1co  5610  f1ocnv  5652  fun11iun  5660  funimass4  5753  fndmdifcom  5815  fsn2  5882  fvtp2g  5924  fvtp3g  5925  fvtp2  5927  fvtp3  5928  riotaeqimp  6063  acexmid  6084  oveqan12rd  6105  cofunex2g  6339  brtposg  6525  tposoprab  6551  smores3  6564  smores2  6565  smoel  6571  tfri3  6638  rdgtfr  6645  rdgruledefgg  6646  omcl  6734  oeicl  6735  nnmsucr  6761  nnmcom  6762  nndir  6763  nnaordi  6781  nnaordr  6783  nnaword  6784  nnmordi  6789  nnaordex  6801  nnm00  6803  ersym  6819  elecg  6847  riinerm  6882  ecopovsym  6905  ecopovsymg  6908  ecovcom  6916  ecovicom  6917  mapvalg  6932  pmvalg  6933  elpmg  6938  elmapssres  6954  pmss12g  6956  ixpconstg  6989  domssr  7064  ener  7066  domtr  7072  f1imaeng  7079  fundmen  7094  xpcomco  7124  xpsnen2g  7127  xpdom2  7129  xpdom1g  7131  enen2  7141  domen2  7143  ssfilem  7177  ssfilemd  7179  diffitest  7191  fiintim  7238  fundmfibi  7252  f1setfi  7317  cnvti  7359  djuex  7383  nnnninf  7466  netap  7620  2omotaplemap  7623  ltsopi  7687  pitric  7688  pitri3or  7689  addcompig  7696  mulcompig  7698  ltapig  7705  ltmpig  7706  nnppipi  7710  addcomnqg  7748  addassnqg  7749  distrnqg  7754  recexnq  7757  nqtri3or  7763  ltmnqg  7768  lt2addnq  7771  lt2mulnq  7772  ltbtwnnqq  7782  prarloclemarch2  7786  enq0ref  7800  distrnq0  7826  mulcomnq0  7827  prcdnql  7851  prcunqu  7852  prarloclemlt  7860  genpassl  7891  genpassu  7892  nqprloc  7912  nqpru  7919  appdiv0nq  7931  addcomprg  7945  mulcomprg  7947  distrlem4prl  7951  distrlem4pru  7952  1idprl  7957  1idpru  7958  ltsopr  7963  recexprlemss1l  8002  recexprlemss1u  8003  gt0srpr  8115  mulcomsrg  8124  ltsosr  8131  aptisr  8146  mulextsr1  8148  map2psrprg  8172  axaddcom  8237  axltwlin  8393  axapti  8396  letri3  8406  eqlelt  8412  mul31  8458  cnegexlem3  8504  subval  8519  subcl  8526  pncan2  8534  pncan3  8535  npcan  8536  addsubeq4  8542  npncan3  8565  negsubdi2  8586  muladd  8712  subdi  8713  mulneg2  8724  mulsub  8729  ltleadd  8775  ltsubpos  8783  posdif  8784  addge01  8801  lesub0  8808  reapneg  8927  prodgt02  9185  prodge02  9187  ltdivmul  9208  lerec  9216  lediv2a  9227  le2msq  9233  msq11  9234  lbreu  9277  dfinfre  9288  creur  9291  creui  9292  cju  9293  indval  9298  nnmulcl  9327  nndivtr  9348  avgle1  9550  avgle2  9551  nn0nnaddcl  9598  zletric  9692  zrevaddcl  9699  znnsub  9700  znn0sub  9714  ltsubnn0  9716  zdclt  9726  zextlt  9742  gtndiv  9745  prime  9749  peano5uzti  9758  uztrn2  9949  uztric  9953  uz11  9954  nn0pzuz  9996  indstr  10002  supinfneg  10004  infsupneg  10005  eluzdc  10019  qrevaddcl  10053  difrp  10103  xrltnsym  10205  xrltso  10208  xrlttri3  10209  xrletri3  10216  xleneg  10249  xaddcom  10273  xposdif  10294  ixxssixx  10314  iccid  10337  iooshf  10364  iccsupr  10378  iooneg  10400  iccneg  10401  fztri3or  10453  fzdcel  10454  fzn  10456  fzen  10457  fzass4  10478  fzrev  10501  fznn  10506  elfzp1b  10514  elfzm1b  10515  fz0fzdiffz0  10547  difelfznle  10552  fzon  10584  fzo0n  10585  fzonmapblen  10609  elfzoextl  10619  eluzgtdifelfzo  10625  ubmelm1fzo  10654  subfzo0  10671  qletric  10686  qdclt  10690  qdcle  10691  ioo0  10704  ico0  10706  ioc0  10707  flqbi  10738  flqbi2  10739  flqzadd  10746  modfzo0difsn  10845  fzfig  10880  expcllem  11000  expap0  11019  mulbinom2  11106  expnbnd  11114  sq11ap  11158  hashfacen  11298  iswrdinn0  11323  ccatsymb  11384  ccatalpha  11395  swrd0g  11446  swrdsbslen  11452  swrdspsleq  11453  wrd2ind  11509  pfxccatin12lem1  11514  pfxccatin12lem2  11517  pfxccatin12  11519  swrdccat3blem  11525  shftlem  11595  shftuz  11596  shftfvalg  11597  ovshftex  11598  shftfval  11600  shftval4  11607  shftval5  11608  2shfti  11610  mulreap  11643  sqrt11ap  11818  abs3dif  11886  abs2difabs  11889  maxabslemval  11989  maxle2  11993  maxclpr  12003  2zsupmax  12007  mingeb  12024  2zinfmin  12025  xrmaxiflemval  12032  xrmax2sup  12036  iooinsup  12059  climshftlemg  12084  fsumcnv  12220  explecnv  12288  geo2lim  12299  prodmodc  12361  fprodcnv  12408  demoivre  12556  demoivreALT  12557  nndivides  12580  0dvds  12594  muldvds1  12599  muldvds2  12600  dvdssubr  12622  dvdsadd2b  12623  odd2np1  12656  mulsucdiv2z  12668  ltoddhalfle  12676  ndvdssub  12713  gcdcom  12766  neggcd  12776  gcdabs2  12783  modgcd  12784  bezoutlemaz  12796  dfgcd2  12807  lcmcom  12858  neglcm  12869  lcmgcdeq  12877  coprmdvds  12886  qredeq  12890  divgcdcoprmex  12896  isprm3  12912  prmind2  12914  dvdsprm  12932  cncongrprm  12952  sqrt2irr  12957  nnmaxpw  12969  hashgcdeq  13038  modprmn0modprm0  13055  coprimeprodsq  13056  pythagtriplem1  13064  pythagtriplem4  13067  pc2dvds  13129  pc11  13130  pcz  13131  pcprod  13145  prmunb  13161  1arithlem2  13163  1arithlem3  13164  1arith  13166  ptex  13667  issubmnd  13804  submcl  13835  resmhm2b  13845  grpinvsub  13936  dfgrp3mlem  13952  imasabl  14189  mgpress  14279  srgmulgass  14342  dfrhm2  14510  isrim0  14517  rmodislmodlem  14736  rmodislmod  14737  cnfldexp  14963  dvdsrzring  14987  znf1o  15035  eltg  15202  eltg2  15203  tgss  15213  tgss2  15229  basgen2  15231  bastop1  15233  opnneiss  15308  cnrest  15385  txss12  15416  hmeofvalg  15453  txswaphmeolem  15470  txswaphmeo  15471  blpnfctr  15589  metequiv  15645  metcnp3  15661  qtopbasss  15671  reopnap  15696  bl2ioo  15700  ioo2bl  15701  ioo2blex  15702  cncfval  15722  divccncfap  15740  addccncf  15750  expcncf  15759  dvexp  15861  dvmptfsum  15875  dvef  15877  efle  15926  reapef  15928  ptolemy  15975  logleb  16027  logdivle  16047  lgsprme0  16259  gausslemma2dlem1a  16275  gausslemma2dlem4  16281  lgsquadlem3  16296  2lgsoddprmlem2  16323  upgrpredgv  16485  uhgr2edg  16545  issubgr  16596  subgrprop  16598  subuhgr  16611  subupgr  16612  subumgr  16613  subusgr  16614  upgriswlkdc  16699  upgrwlkvtxedg  16703  g0wlk0  16709  clwwlkn1  16757  clwwlknonex2lem2  16777  dichmul0orlem3  16853  uzdcinzz  16924  exmidsbthrlem  17165  triap  17176