Theorem ancoms 268

Description: Inference commuting conjunction in antecedent. (Contributed by NM, 21-Apr-1994.)

Hypothesis

Ref	Expression
ancoms.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
ancoms	⊢ ((𝜓 ∧ 𝜑) → 𝜒)

Proof of Theorem ancoms

Step	Hyp	Ref	Expression
1		ancoms.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	expcom 116	. 2 ⊢ (𝜓 → (𝜑 → 𝜒))
3	2	imp 124	1 ⊢ ((𝜓 ∧ 𝜑) → 𝜒)

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  579  anabsi7  583  anabsi8  584  im2anan9r  603  bi2anan9r  611  syl3anr2  1326  mp3anr1  1370  mp3anr2  1371  mp3anr3  1372  stoic1b  1472  cbvaldvaw  1979  eu5  2127  2exeu  2172  eqeqan12rd  2248  sylan9eqr  2286  r19.29vva  2678  morex  2990  sylan9ssr  3241  riinm  4043  breqan12rd  4105  elnn  4704  soinxp  4796  seinxp  4797  brelrng  4963  dminss  5151  imainss  5152  funsng  5376  funcnvuni  5399  f1co  5554  f1ocnv  5596  fun11iun  5604  funimass4  5696  fndmdifcom  5753  fsn2  5821  fvtp2g  5863  fvtp3g  5864  fvtp2  5866  fvtp3  5867  riotaeqimp  5996  acexmid  6017  oveqan12rd  6038  cofunex2g  6272  brtposg  6420  tposoprab  6446  smores3  6459  smores2  6460  smoel  6466  tfri3  6533  rdgtfr  6540  rdgruledefgg  6541  omcl  6629  oeicl  6630  nnmsucr  6656  nnmcom  6657  nndir  6658  nnaordi  6676  nnaordr  6678  nnaword  6679  nnmordi  6684  nnaordex  6696  nnm00  6698  ersym  6714  elecg  6742  riinerm  6777  ecopovsym  6800  ecopovsymg  6803  ecovcom  6811  ecovicom  6812  mapvalg  6827  pmvalg  6828  elpmg  6833  elmapssres  6842  pmss12g  6844  ixpconstg  6876  domssr  6951  ener  6953  domtr  6959  f1imaeng  6966  fundmen  6981  xpcomco  7010  xpsnen2g  7013  xpdom2  7015  xpdom1g  7017  enen2  7027  domen2  7029  ssfilem  7062  ssfilemd  7064  diffitest  7076  fiintim  7123  fundmfibi  7137  cnvti  7218  djuex  7242  nnnninf  7325  netap  7473  2omotaplemap  7476  ltsopi  7540  pitric  7541  pitri3or  7542  addcompig  7549  mulcompig  7551  ltapig  7558  ltmpig  7559  nnppipi  7563  addcomnqg  7601  addassnqg  7602  distrnqg  7607  recexnq  7610  nqtri3or  7616  ltmnqg  7621  lt2addnq  7624  lt2mulnq  7625  ltbtwnnqq  7635  prarloclemarch2  7639  enq0ref  7653  distrnq0  7679  mulcomnq0  7680  prcdnql  7704  prcunqu  7705  prarloclemlt  7713  genpassl  7744  genpassu  7745  nqprloc  7765  nqpru  7772  appdiv0nq  7784  addcomprg  7798  mulcomprg  7800  distrlem4prl  7804  distrlem4pru  7805  1idprl  7810  1idpru  7811  ltsopr  7816  recexprlemss1l  7855  recexprlemss1u  7856  gt0srpr  7968  mulcomsrg  7977  ltsosr  7984  aptisr  7999  mulextsr1  8001  map2psrprg  8025  axaddcom  8090  axltwlin  8247  axapti  8250  letri3  8260  eqlelt  8266  mul31  8310  cnegexlem3  8356  subval  8371  subcl  8378  pncan2  8386  pncan3  8387  npcan  8388  addsubeq4  8394  npncan3  8417  negsubdi2  8438  muladd  8563  subdi  8564  mulneg2  8575  mulsub  8580  ltleadd  8626  ltsubpos  8634  posdif  8635  addge01  8652  lesub0  8659  reapneg  8777  prodgt02  9033  prodge02  9035  ltdivmul  9056  lerec  9064  lediv2a  9075  le2msq  9081  msq11  9082  lbreu  9125  dfinfre  9136  creur  9139  creui  9140  cju  9141  nnmulcl  9164  nndivtr  9185  avgle1  9385  avgle2  9386  nn0nnaddcl  9433  zletric  9523  zrevaddcl  9530  znnsub  9531  znn0sub  9545  ltsubnn0  9547  zdclt  9557  zextlt  9572  gtndiv  9575  prime  9579  peano5uzti  9588  uztrn2  9774  uztric  9778  uz11  9779  nn0pzuz  9821  indstr  9827  supinfneg  9829  infsupneg  9830  eluzdc  9844  qrevaddcl  9878  difrp  9927  xrltnsym  10028  xrltso  10031  xrlttri3  10032  xrletri3  10039  xleneg  10072  xaddcom  10096  xposdif  10117  ixxssixx  10137  iccid  10160  iooshf  10187  iccsupr  10201  iooneg  10223  iccneg  10224  fztri3or  10274  fzdcel  10275  fzn  10277  fzen  10278  fzass4  10297  fzrev  10319  fznn  10324  elfzp1b  10332  elfzm1b  10333  fz0fzdiffz0  10365  difelfznle  10370  fzon  10402  fzo0n  10403  fzonmapblen  10427  elfzoextl  10437  eluzgtdifelfzo  10443  ubmelm1fzo  10472  subfzo0  10489  qletric  10502  qdclt  10506  qdcle  10507  ioo0  10520  ico0  10522  ioc0  10523  flqbi  10551  flqbi2  10552  flqzadd  10559  modfzo0difsn  10658  fzfig  10693  expcllem  10813  expap0  10832  mulbinom2  10919  expnbnd  10926  sq11ap  10970  hashfacen  11101  iswrdinn0  11119  ccatsymb  11180  ccatalpha  11191  swrd0g  11242  swrdsbslen  11248  swrdspsleq  11249  wrd2ind  11305  pfxccatin12lem1  11310  pfxccatin12lem2  11313  pfxccatin12  11315  swrdccat3blem  11321  shftlem  11378  shftuz  11379  shftfvalg  11380  ovshftex  11381  shftfval  11383  shftval4  11390  shftval5  11391  2shfti  11393  mulreap  11426  sqrt11ap  11600  abs3dif  11667  abs2difabs  11670  maxabslemval  11770  maxle2  11774  maxclpr  11784  2zsupmax  11788  mingeb  11804  2zinfmin  11805  xrmaxiflemval  11812  xrmax2sup  11816  iooinsup  11839  climshftlemg  11864  fsumcnv  12000  explecnv  12068  geo2lim  12079  prodmodc  12141  fprodcnv  12188  demoivre  12336  demoivreALT  12337  nndivides  12360  0dvds  12374  muldvds1  12379  muldvds2  12380  dvdssubr  12402  dvdsadd2b  12403  odd2np1  12436  mulsucdiv2z  12448  ltoddhalfle  12456  ndvdssub  12493  gcdcom  12546  neggcd  12556  gcdabs2  12563  modgcd  12564  bezoutlemaz  12576  dfgcd2  12587  lcmcom  12638  neglcm  12649  lcmgcdeq  12657  coprmdvds  12666  qredeq  12670  divgcdcoprmex  12676  isprm3  12692  prmind2  12694  dvdsprm  12711  cncongrprm  12731  sqrt2irr  12736  hashgcdeq  12814  modprmn0modprm0  12831  coprimeprodsq  12832  pythagtriplem1  12840  pythagtriplem4  12843  pc2dvds  12905  pc11  12906  pcz  12907  pcprod  12921  prmunb  12937  1arithlem2  12939  1arithlem3  12940  1arith  12942  ptex  13349  issubmnd  13527  submcl  13564  resmhm2b  13574  grpinvsub  13667  dfgrp3mlem  13683  imasabl  13925  mgpress  13947  srgmulgass  14005  dfrhm2  14171  isrim0  14178  rmodislmodlem  14367  rmodislmod  14368  cnfldexp  14594  dvdsrzring  14620  znf1o  14668  eltg  14779  eltg2  14780  tgss  14790  tgss2  14806  basgen2  14808  bastop1  14810  opnneiss  14885  cnrest  14962  txss12  14993  hmeofvalg  15030  txswaphmeolem  15047  txswaphmeo  15048  blpnfctr  15166  metequiv  15222  metcnp3  15238  qtopbasss  15248  reopnap  15273  bl2ioo  15277  ioo2bl  15278  ioo2blex  15279  cncfval  15299  divccncfap  15317  addccncf  15327  expcncf  15336  dvexp  15438  dvmptfsum  15452  dvef  15454  efle  15503  reapef  15505  ptolemy  15551  logleb  15602  lgsprme0  15774  gausslemma2dlem1a  15790  gausslemma2dlem4  15796  lgsquadlem3  15811  2lgsoddprmlem2  15838  upgrpredgv  16000  uhgr2edg  16060  issubgr  16111  subgrprop  16113  subuhgr  16126  subupgr  16127  subumgr  16128  subusgr  16129  upgriswlkdc  16214  upgrwlkvtxedg  16218  g0wlk0  16224  clwwlkn1  16272  clwwlknonex2lem2  16292  uzdcinzz  16415  exmidsbthrlem  16647  triap  16654