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  4148  elnn  4755  soinxp  4847  seinxp  4848  brelrng  5015  dminss  5205  imainss  5206  funsng  5430  funcnvuni  5453  f1co  5613  f1ocnv  5655  fun11iun  5663  funimass4  5756  fndmdifcom  5818  fsn2  5885  fvtp2g  5927  fvtp3g  5928  fvtp2  5930  fvtp3  5931  riotaeqimp  6066  acexmid  6087  oveqan12rd  6108  cofunex2g  6343  brtposg  6530  tposoprab  6556  smores3  6569  smores2  6570  smoel  6576  tfri3  6643  rdgtfr  6650  rdgruledefgg  6651  omcl  6739  oeicl  6740  nnmsucr  6766  nnmcom  6767  nndir  6768  nnaordi  6786  nnaordr  6788  nnaword  6789  nnmordi  6794  nnaordex  6806  nnm00  6808  ersym  6824  elecg  6852  riinerm  6887  ecopovsym  6910  ecopovsymg  6913  ecovcom  6921  ecovicom  6922  mapvalg  6937  pmvalg  6938  elpmg  6943  elmapssres  6959  pmss12g  6961  ixpconstg  6995  domssr  7070  ener  7072  domtr  7078  f1imaeng  7085  fundmen  7100  xpcomco  7130  xpsnen2g  7133  xpdom2  7135  xpdom1g  7137  enen2  7147  domen2  7149  ssfilem  7183  ssfilemd  7185  diffitest  7197  fiintim  7244  fundmfibi  7258  f1setfi  7322  cnvti  7365  djuex  7389  nnnninf  7472  netap  7626  2omotaplemap  7629  ltsopi  7693  pitric  7694  pitri3or  7695  addcompig  7702  mulcompig  7704  ltapig  7711  ltmpig  7712  nnppipi  7716  addcomnqg  7754  addassnqg  7755  distrnqg  7760  recexnq  7763  nqtri3or  7769  ltmnqg  7774  lt2addnq  7777  lt2mulnq  7778  ltbtwnnqq  7788  prarloclemarch2  7792  enq0ref  7806  distrnq0  7832  mulcomnq0  7833  prcdnql  7857  prcunqu  7858  prarloclemlt  7866  genpassl  7897  genpassu  7898  nqprloc  7918  nqpru  7925  appdiv0nq  7937  addcomprg  7951  mulcomprg  7953  distrlem4prl  7957  distrlem4pru  7958  1idprl  7963  1idpru  7964  ltsopr  7969  recexprlemss1l  8008  recexprlemss1u  8009  gt0srpr  8121  mulcomsrg  8130  ltsosr  8137  aptisr  8152  mulextsr1  8154  map2psrprg  8178  axaddcom  8243  axltwlin  8399  axapti  8402  letri3  8412  eqlelt  8418  mul31  8464  cnegexlem3  8510  subval  8525  subcl  8532  pncan2  8540  pncan3  8541  npcan  8542  addsubeq4  8548  npncan3  8571  negsubdi2  8592  muladd  8718  subdi  8719  mulneg2  8730  mulsub  8735  ltleadd  8781  ltsubpos  8789  posdif  8790  addge01  8807  lesub0  8814  reapneg  8933  prodgt02  9191  prodge02  9193  ltdivmul  9214  lerec  9222  lediv2a  9233  le2msq  9239  msq11  9240  lbreu  9283  dfinfre  9294  creur  9297  creui  9298  cju  9299  indval  9305  nnmulcl  9334  nndivtr  9355  avgle1  9557  avgle2  9558  nn0nnaddcl  9605  zletric  9697  zrevaddcl  9704  znnsub  9705  znn0sub  9719  ltsubnn0  9721  zdclt  9731  zextlt  9748  gtndiv  9751  prime  9755  peano5uzti  9764  uztrn2  9955  uztric  9959  uz11  9960  nn0pzuz  10002  indstr  10008  supinfneg  10010  infsupneg  10011  eluzdc  10025  qrevaddcl  10059  difrp  10109  xrltnsym  10211  xrltso  10214  xrlttri3  10215  xrletri3  10222  xleneg  10255  xaddcom  10279  xposdif  10300  ixxssixx  10320  iccid  10343  iooshf  10370  iccsupr  10384  iooneg  10406  iccneg  10407  fztri3or  10459  fzdcel  10460  fzn  10462  fzen  10463  fzass4  10484  fzrev  10507  fznn  10512  elfzp1b  10520  elfzm1b  10521  fz0fzdiffz0  10553  difelfznle  10558  fzon  10590  fzo0n  10591  fzonmapblen  10615  elfzoextl  10625  eluzgtdifelfzo  10631  ubmelm1fzo  10660  subfzo0  10677  qletric  10692  qdclt  10696  qdcle  10697  ioo0  10710  ico0  10712  ioc0  10713  flqbi  10745  flqbi2  10746  flqzadd  10753  modfzo0difsn  10852  fzfig  10887  expcllem  11007  expap0  11026  mulbinom2  11113  expnbnd  11121  sq11ap  11165  hashfacen  11305  iswrdinn0  11330  ccatsymb  11391  ccatalpha  11402  swrd0g  11453  swrdsbslen  11459  swrdspsleq  11460  wrd2ind  11516  pfxccatin12lem1  11521  pfxccatin12lem2  11524  pfxccatin12  11526  swrdccat3blem  11532  shftlem  11602  shftuz  11603  shftfvalg  11604  ovshftex  11605  shftfval  11607  shftval4  11614  shftval5  11615  2shfti  11617  mulreap  11650  sqrt11ap  11825  abs3dif  11893  abs2difabs  11896  maxabslemval  11996  maxle2  12000  maxclpr  12010  2zsupmax  12014  mingeb  12032  2zinfmin  12033  xrmaxiflemval  12040  xrmax2sup  12044  iooinsup  12067  climshftlemg  12092  fsumcnv  12228  explecnv  12296  geo2lim  12307  prodmodc  12369  fprodcnv  12416  demoivre  12564  demoivreALT  12565  nndivides  12588  0dvds  12602  muldvds1  12607  muldvds2  12608  dvdssubr  12630  dvdsadd2b  12631  odd2np1  12664  mulsucdiv2z  12676  ltoddhalfle  12684  ndvdssub  12721  gcdcom  12774  neggcd  12784  gcdabs2  12791  modgcd  12792  bezoutlemaz  12804  dfgcd2  12815  lcmcom  12866  neglcm  12877  lcmgcdeq  12885  coprmdvds  12894  qredeq  12898  divgcdcoprmex  12904  isprm3  12920  prmind2  12922  dvdsprm  12940  cncongrprm  12960  sqrt2irr  12965  nnmaxpw  12977  hashgcdeq  13046  modprmn0modprm0  13063  coprimeprodsq  13064  pythagtriplem1  13072  pythagtriplem4  13075  pc2dvds  13137  pc11  13138  pcz  13139  pcprod  13153  prmunb  13169  1arithlem2  13171  1arithlem3  13172  1arith  13174  ptex  13676  issubmnd  13813  submcl  13844  resmhm2b  13854  grpinvsub  13945  dfgrp3mlem  13961  cntz2ss  14167  cntzrec  14168  imasabl  14229  mgpress  14336  srgmulgass  14399  dfrhm2  14569  isrim0  14576  rmodislmodlem  14795  rmodislmod  14796  cnfldexp  15022  dvdsrzring  15046  znf1o  15094  eltg  15295  eltg2  15296  tgss  15306  tgss2  15322  basgen2  15324  bastop1  15326  opnneiss  15401  cnrest  15478  txss12  15509  hmeofvalg  15546  txswaphmeolem  15563  txswaphmeo  15564  blpnfctr  15682  metequiv  15738  metcnp3  15754  qtopbasss  15764  reopnap  15789  bl2ioo  15793  ioo2bl  15794  ioo2blex  15795  cncfval  15815  divccncfap  15833  addccncf  15843  expcncf  15852  dvexp  15954  dvmptfsum  15968  dvef  15970  efle  16019  reapef  16021  ptolemy  16068  logleb  16122  logdivle  16142  lgsprme0  16383  gausslemma2dlem1a  16399  gausslemma2dlem4  16405  lgsquadlem3  16420  2lgsoddprmlem2  16447  upgrpredgv  16609  uhgr2edg  16669  issubgr  16720  subgrprop  16722  subuhgr  16735  subupgr  16736  subumgr  16737  subusgr  16738  upgriswlkdc  16823  upgrwlkvtxedg  16827  g0wlk0  16833  clwwlkn1  16881  clwwlknonex2lem2  16901  dichmul0orlem3  16977  uzdcinzz  17048  exmidsbthrlem  17290  triap  17301