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  8457  cnegexlem3  8503  subval  8518  subcl  8525  pncan2  8533  pncan3  8534  npcan  8535  addsubeq4  8541  npncan3  8564  negsubdi2  8585  muladd  8711  subdi  8712  mulneg2  8723  mulsub  8728  ltleadd  8774  ltsubpos  8782  posdif  8783  addge01  8800  lesub0  8807  reapneg  8925  prodgt02  9183  prodge02  9185  ltdivmul  9206  lerec  9214  lediv2a  9225  le2msq  9231  msq11  9232  lbreu  9275  dfinfre  9286  creur  9289  creui  9290  cju  9291  indval  9296  nnmulcl  9325  nndivtr  9346  avgle1  9546  avgle2  9547  nn0nnaddcl  9594  zletric  9688  zrevaddcl  9695  znnsub  9696  znn0sub  9710  ltsubnn0  9712  zdclt  9722  zextlt  9738  gtndiv  9741  prime  9745  peano5uzti  9754  uztrn2  9940  uztric  9944  uz11  9945  nn0pzuz  9987  indstr  9993  supinfneg  9995  infsupneg  9996  eluzdc  10010  qrevaddcl  10044  difrp  10093  xrltnsym  10195  xrltso  10198  xrlttri3  10199  xrletri3  10206  xleneg  10239  xaddcom  10263  xposdif  10284  ixxssixx  10304  iccid  10327  iooshf  10354  iccsupr  10368  iooneg  10390  iccneg  10391  fztri3or  10443  fzdcel  10444  fzn  10446  fzen  10447  fzass4  10468  fzrev  10491  fznn  10496  elfzp1b  10504  elfzm1b  10505  fz0fzdiffz0  10537  difelfznle  10542  fzon  10574  fzo0n  10575  fzonmapblen  10599  elfzoextl  10609  eluzgtdifelfzo  10615  ubmelm1fzo  10644  subfzo0  10661  qletric  10676  qdclt  10680  qdcle  10681  ioo0  10694  ico0  10696  ioc0  10697  flqbi  10725  flqbi2  10726  flqzadd  10733  modfzo0difsn  10832  fzfig  10867  expcllem  10987  expap0  11006  mulbinom2  11093  expnbnd  11101  sq11ap  11145  hashfacen  11284  iswrdinn0  11309  ccatsymb  11370  ccatalpha  11381  swrd0g  11432  swrdsbslen  11438  swrdspsleq  11439  wrd2ind  11495  pfxccatin12lem1  11500  pfxccatin12lem2  11503  pfxccatin12  11505  swrdccat3blem  11511  shftlem  11581  shftuz  11582  shftfvalg  11583  ovshftex  11584  shftfval  11586  shftval4  11593  shftval5  11594  2shfti  11596  mulreap  11629  sqrt11ap  11804  abs3dif  11871  abs2difabs  11874  maxabslemval  11974  maxle2  11978  maxclpr  11988  2zsupmax  11992  mingeb  12008  2zinfmin  12009  xrmaxiflemval  12016  xrmax2sup  12020  iooinsup  12043  climshftlemg  12068  fsumcnv  12204  explecnv  12272  geo2lim  12283  prodmodc  12345  fprodcnv  12392  demoivre  12540  demoivreALT  12541  nndivides  12564  0dvds  12578  muldvds1  12583  muldvds2  12584  dvdssubr  12606  dvdsadd2b  12607  odd2np1  12640  mulsucdiv2z  12652  ltoddhalfle  12660  ndvdssub  12697  gcdcom  12750  neggcd  12760  gcdabs2  12767  modgcd  12768  bezoutlemaz  12780  dfgcd2  12791  lcmcom  12842  neglcm  12853  lcmgcdeq  12861  coprmdvds  12870  qredeq  12874  divgcdcoprmex  12880  isprm3  12896  prmind2  12898  dvdsprm  12915  cncongrprm  12935  sqrt2irr  12940  hashgcdeq  13018  modprmn0modprm0  13035  coprimeprodsq  13036  pythagtriplem1  13044  pythagtriplem4  13047  pc2dvds  13109  pc11  13110  pcz  13111  pcprod  13125  prmunb  13141  1arithlem2  13143  1arithlem3  13144  1arith  13146  ptex  13618  issubmnd  13755  submcl  13786  resmhm2b  13796  grpinvsub  13887  dfgrp3mlem  13903  imasabl  14140  mgpress  14230  srgmulgass  14293  dfrhm2  14461  isrim0  14468  rmodislmodlem  14687  rmodislmod  14688  cnfldexp  14914  dvdsrzring  14938  znf1o  14986  eltg  15153  eltg2  15154  tgss  15164  tgss2  15180  basgen2  15182  bastop1  15184  opnneiss  15259  cnrest  15336  txss12  15367  hmeofvalg  15404  txswaphmeolem  15421  txswaphmeo  15422  blpnfctr  15540  metequiv  15596  metcnp3  15612  qtopbasss  15622  reopnap  15647  bl2ioo  15651  ioo2bl  15652  ioo2blex  15653  cncfval  15673  divccncfap  15691  addccncf  15701  expcncf  15710  dvexp  15812  dvmptfsum  15826  dvef  15828  efle  15877  reapef  15879  ptolemy  15925  logleb  15976  lgsprme0  16161  gausslemma2dlem1a  16177  gausslemma2dlem4  16183  lgsquadlem3  16198  2lgsoddprmlem2  16225  upgrpredgv  16387  uhgr2edg  16447  issubgr  16498  subgrprop  16500  subuhgr  16513  subupgr  16514  subumgr  16515  subusgr  16516  upgriswlkdc  16601  upgrwlkvtxedg  16605  g0wlk0  16611  clwwlkn1  16659  clwwlknonex2lem2  16679  dichmul0orlem3  16755  uzdcinzz  16826  exmidsbthrlem  17067  triap  17078