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  1327  mp3anr1  1371  mp3anr2  1372  mp3anr3  1373  stoic1b  1473  cbvaldvaw  1980  eu5  2128  2exeu  2173  eqeqan12rd  2249  sylan9eqr  2287  r19.29vva  2688  morex  3000  sylan9ssr  3251  riinm  4063  breqan12rd  4125  elnn  4727  soinxp  4819  seinxp  4820  brelrng  4987  dminss  5176  imainss  5177  funsng  5401  funcnvuni  5424  f1co  5584  f1ocnv  5626  fun11iun  5634  funimass4  5726  fndmdifcom  5783  fsn2  5850  fvtp2g  5892  fvtp3g  5893  fvtp2  5895  fvtp3  5896  riotaeqimp  6027  acexmid  6048  oveqan12rd  6069  cofunex2g  6302  brtposg  6484  tposoprab  6510  smores3  6523  smores2  6524  smoel  6530  tfri3  6597  rdgtfr  6604  rdgruledefgg  6605  omcl  6693  oeicl  6694  nnmsucr  6720  nnmcom  6721  nndir  6722  nnaordi  6740  nnaordr  6742  nnaword  6743  nnmordi  6748  nnaordex  6760  nnm00  6762  ersym  6778  elecg  6806  riinerm  6841  ecopovsym  6864  ecopovsymg  6867  ecovcom  6875  ecovicom  6876  mapvalg  6891  pmvalg  6892  elpmg  6897  elmapssres  6906  pmss12g  6908  ixpconstg  6941  domssr  7016  ener  7018  domtr  7024  f1imaeng  7031  fundmen  7046  xpcomco  7076  xpsnen2g  7079  xpdom2  7081  xpdom1g  7083  enen2  7093  domen2  7095  ssfilem  7129  ssfilemd  7131  diffitest  7143  fiintim  7190  fundmfibi  7204  cnvti  7309  djuex  7333  nnnninf  7416  netap  7567  2omotaplemap  7570  ltsopi  7634  pitric  7635  pitri3or  7636  addcompig  7643  mulcompig  7645  ltapig  7652  ltmpig  7653  nnppipi  7657  addcomnqg  7695  addassnqg  7696  distrnqg  7701  recexnq  7704  nqtri3or  7710  ltmnqg  7715  lt2addnq  7718  lt2mulnq  7719  ltbtwnnqq  7729  prarloclemarch2  7733  enq0ref  7747  distrnq0  7773  mulcomnq0  7774  prcdnql  7798  prcunqu  7799  prarloclemlt  7807  genpassl  7838  genpassu  7839  nqprloc  7859  nqpru  7866  appdiv0nq  7878  addcomprg  7892  mulcomprg  7894  distrlem4prl  7898  distrlem4pru  7899  1idprl  7904  1idpru  7905  ltsopr  7910  recexprlemss1l  7949  recexprlemss1u  7950  gt0srpr  8062  mulcomsrg  8071  ltsosr  8078  aptisr  8093  mulextsr1  8095  map2psrprg  8119  axaddcom  8184  axltwlin  8340  axapti  8343  letri3  8353  eqlelt  8359  mul31  8403  cnegexlem3  8449  subval  8464  subcl  8471  pncan2  8479  pncan3  8480  npcan  8481  addsubeq4  8487  npncan3  8510  negsubdi2  8531  muladd  8656  subdi  8657  mulneg2  8668  mulsub  8673  ltleadd  8719  ltsubpos  8727  posdif  8728  addge01  8745  lesub0  8752  reapneg  8870  prodgt02  9126  prodge02  9128  ltdivmul  9149  lerec  9157  lediv2a  9168  le2msq  9174  msq11  9175  lbreu  9218  dfinfre  9229  creur  9232  creui  9233  cju  9234  nnmulcl  9257  nndivtr  9278  avgle1  9478  avgle2  9479  nn0nnaddcl  9526  zletric  9620  zrevaddcl  9627  znnsub  9628  znn0sub  9642  ltsubnn0  9644  zdclt  9654  zextlt  9669  gtndiv  9672  prime  9676  peano5uzti  9685  uztrn2  9871  uztric  9875  uz11  9876  nn0pzuz  9918  indstr  9924  supinfneg  9926  infsupneg  9927  eluzdc  9941  qrevaddcl  9975  difrp  10024  xrltnsym  10125  xrltso  10128  xrlttri3  10129  xrletri3  10136  xleneg  10169  xaddcom  10193  xposdif  10214  ixxssixx  10234  iccid  10257  iooshf  10284  iccsupr  10298  iooneg  10320  iccneg  10321  fztri3or  10372  fzdcel  10373  fzn  10375  fzen  10376  fzass4  10395  fzrev  10417  fznn  10422  elfzp1b  10430  elfzm1b  10431  fz0fzdiffz0  10463  difelfznle  10468  fzon  10500  fzo0n  10501  fzonmapblen  10525  elfzoextl  10535  eluzgtdifelfzo  10541  ubmelm1fzo  10570  subfzo0  10587  qletric  10600  qdclt  10604  qdcle  10605  ioo0  10618  ico0  10620  ioc0  10621  flqbi  10649  flqbi2  10650  flqzadd  10657  modfzo0difsn  10756  fzfig  10791  expcllem  10911  expap0  10930  mulbinom2  11017  expnbnd  11024  sq11ap  11068  hashfacen  11204  iswrdinn0  11225  ccatsymb  11286  ccatalpha  11297  swrd0g  11348  swrdsbslen  11354  swrdspsleq  11355  wrd2ind  11411  pfxccatin12lem1  11416  pfxccatin12lem2  11419  pfxccatin12  11421  swrdccat3blem  11427  shftlem  11497  shftuz  11498  shftfvalg  11499  ovshftex  11500  shftfval  11502  shftval4  11509  shftval5  11510  2shfti  11512  mulreap  11545  sqrt11ap  11719  abs3dif  11786  abs2difabs  11789  maxabslemval  11889  maxle2  11893  maxclpr  11903  2zsupmax  11907  mingeb  11923  2zinfmin  11924  xrmaxiflemval  11931  xrmax2sup  11935  iooinsup  11958  climshftlemg  11983  fsumcnv  12119  explecnv  12187  geo2lim  12198  prodmodc  12260  fprodcnv  12307  demoivre  12455  demoivreALT  12456  nndivides  12479  0dvds  12493  muldvds1  12498  muldvds2  12499  dvdssubr  12521  dvdsadd2b  12522  odd2np1  12555  mulsucdiv2z  12567  ltoddhalfle  12575  ndvdssub  12612  gcdcom  12665  neggcd  12675  gcdabs2  12682  modgcd  12683  bezoutlemaz  12695  dfgcd2  12706  lcmcom  12757  neglcm  12768  lcmgcdeq  12776  coprmdvds  12785  qredeq  12789  divgcdcoprmex  12795  isprm3  12811  prmind2  12813  dvdsprm  12830  cncongrprm  12850  sqrt2irr  12855  hashgcdeq  12933  modprmn0modprm0  12950  coprimeprodsq  12951  pythagtriplem1  12959  pythagtriplem4  12962  pc2dvds  13024  pc11  13025  pcz  13026  pcprod  13040  prmunb  13056  1arithlem2  13058  1arithlem3  13059  1arith  13061  ptex  13469  issubmnd  13647  submcl  13684  resmhm2b  13694  grpinvsub  13787  dfgrp3mlem  13803  imasabl  14045  mgpress  14067  srgmulgass  14125  dfrhm2  14291  isrim0  14298  rmodislmodlem  14490  rmodislmod  14491  cnfldexp  14717  dvdsrzring  14743  znf1o  14791  eltg  14909  eltg2  14910  tgss  14920  tgss2  14936  basgen2  14938  bastop1  14940  opnneiss  15015  cnrest  15092  txss12  15123  hmeofvalg  15160  txswaphmeolem  15177  txswaphmeo  15178  blpnfctr  15296  metequiv  15352  metcnp3  15368  qtopbasss  15378  reopnap  15403  bl2ioo  15407  ioo2bl  15408  ioo2blex  15409  cncfval  15429  divccncfap  15447  addccncf  15457  expcncf  15466  dvexp  15568  dvmptfsum  15582  dvef  15584  efle  15633  reapef  15635  ptolemy  15681  logleb  15732  lgsprme0  15907  gausslemma2dlem1a  15923  gausslemma2dlem4  15929  lgsquadlem3  15944  2lgsoddprmlem2  15971  upgrpredgv  16133  uhgr2edg  16193  issubgr  16244  subgrprop  16246  subuhgr  16259  subupgr  16260  subumgr  16261  subusgr  16262  upgriswlkdc  16347  upgrwlkvtxedg  16351  g0wlk0  16357  clwwlkn1  16405  clwwlknonex2lem2  16425  uzdcinzz  16562  exmidsbthrlem  16794  triap  16805