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  1979  eu5  2127  2exeu  2172  eqeqan12rd  2248  sylan9eqr  2286  r19.29vva  2679  morex  2991  sylan9ssr  3242  riinm  4048  breqan12rd  4110  elnn  4710  soinxp  4802  seinxp  4803  brelrng  4969  dminss  5158  imainss  5159  funsng  5383  funcnvuni  5406  f1co  5563  f1ocnv  5605  fun11iun  5613  funimass4  5705  fndmdifcom  5762  fsn2  5829  fvtp2g  5871  fvtp3g  5872  fvtp2  5874  fvtp3  5875  riotaeqimp  6006  acexmid  6027  oveqan12rd  6048  cofunex2g  6281  brtposg  6463  tposoprab  6489  smores3  6502  smores2  6503  smoel  6509  tfri3  6576  rdgtfr  6583  rdgruledefgg  6584  omcl  6672  oeicl  6673  nnmsucr  6699  nnmcom  6700  nndir  6701  nnaordi  6719  nnaordr  6721  nnaword  6722  nnmordi  6727  nnaordex  6739  nnm00  6741  ersym  6757  elecg  6785  riinerm  6820  ecopovsym  6843  ecopovsymg  6846  ecovcom  6854  ecovicom  6855  mapvalg  6870  pmvalg  6871  elpmg  6876  elmapssres  6885  pmss12g  6887  ixpconstg  6919  domssr  6994  ener  6996  domtr  7002  f1imaeng  7009  fundmen  7024  xpcomco  7053  xpsnen2g  7056  xpdom2  7058  xpdom1g  7060  enen2  7070  domen2  7072  ssfilem  7105  ssfilemd  7107  diffitest  7119  fiintim  7166  fundmfibi  7180  cnvti  7261  djuex  7285  nnnninf  7368  netap  7516  2omotaplemap  7519  ltsopi  7583  pitric  7584  pitri3or  7585  addcompig  7592  mulcompig  7594  ltapig  7601  ltmpig  7602  nnppipi  7606  addcomnqg  7644  addassnqg  7645  distrnqg  7650  recexnq  7653  nqtri3or  7659  ltmnqg  7664  lt2addnq  7667  lt2mulnq  7668  ltbtwnnqq  7678  prarloclemarch2  7682  enq0ref  7696  distrnq0  7722  mulcomnq0  7723  prcdnql  7747  prcunqu  7748  prarloclemlt  7756  genpassl  7787  genpassu  7788  nqprloc  7808  nqpru  7815  appdiv0nq  7827  addcomprg  7841  mulcomprg  7843  distrlem4prl  7847  distrlem4pru  7848  1idprl  7853  1idpru  7854  ltsopr  7859  recexprlemss1l  7898  recexprlemss1u  7899  gt0srpr  8011  mulcomsrg  8020  ltsosr  8027  aptisr  8042  mulextsr1  8044  map2psrprg  8068  axaddcom  8133  axltwlin  8290  axapti  8293  letri3  8303  eqlelt  8309  mul31  8353  cnegexlem3  8399  subval  8414  subcl  8421  pncan2  8429  pncan3  8430  npcan  8431  addsubeq4  8437  npncan3  8460  negsubdi2  8481  muladd  8606  subdi  8607  mulneg2  8618  mulsub  8623  ltleadd  8669  ltsubpos  8677  posdif  8678  addge01  8695  lesub0  8702  reapneg  8820  prodgt02  9076  prodge02  9078  ltdivmul  9099  lerec  9107  lediv2a  9118  le2msq  9124  msq11  9125  lbreu  9168  dfinfre  9179  creur  9182  creui  9183  cju  9184  nnmulcl  9207  nndivtr  9228  avgle1  9428  avgle2  9429  nn0nnaddcl  9476  zletric  9566  zrevaddcl  9573  znnsub  9574  znn0sub  9588  ltsubnn0  9590  zdclt  9600  zextlt  9615  gtndiv  9618  prime  9622  peano5uzti  9631  uztrn2  9817  uztric  9821  uz11  9822  nn0pzuz  9864  indstr  9870  supinfneg  9872  infsupneg  9873  eluzdc  9887  qrevaddcl  9921  difrp  9970  xrltnsym  10071  xrltso  10074  xrlttri3  10075  xrletri3  10082  xleneg  10115  xaddcom  10139  xposdif  10160  ixxssixx  10180  iccid  10203  iooshf  10230  iccsupr  10244  iooneg  10266  iccneg  10267  fztri3or  10317  fzdcel  10318  fzn  10320  fzen  10321  fzass4  10340  fzrev  10362  fznn  10367  elfzp1b  10375  elfzm1b  10376  fz0fzdiffz0  10408  difelfznle  10413  fzon  10445  fzo0n  10446  fzonmapblen  10470  elfzoextl  10480  eluzgtdifelfzo  10486  ubmelm1fzo  10515  subfzo0  10532  qletric  10545  qdclt  10549  qdcle  10550  ioo0  10563  ico0  10565  ioc0  10566  flqbi  10594  flqbi2  10595  flqzadd  10602  modfzo0difsn  10701  fzfig  10736  expcllem  10856  expap0  10875  mulbinom2  10962  expnbnd  10969  sq11ap  11013  hashfacen  11144  iswrdinn0  11165  ccatsymb  11226  ccatalpha  11237  swrd0g  11288  swrdsbslen  11294  swrdspsleq  11295  wrd2ind  11351  pfxccatin12lem1  11356  pfxccatin12lem2  11359  pfxccatin12  11361  swrdccat3blem  11367  shftlem  11437  shftuz  11438  shftfvalg  11439  ovshftex  11440  shftfval  11442  shftval4  11449  shftval5  11450  2shfti  11452  mulreap  11485  sqrt11ap  11659  abs3dif  11726  abs2difabs  11729  maxabslemval  11829  maxle2  11833  maxclpr  11843  2zsupmax  11847  mingeb  11863  2zinfmin  11864  xrmaxiflemval  11871  xrmax2sup  11875  iooinsup  11898  climshftlemg  11923  fsumcnv  12059  explecnv  12127  geo2lim  12138  prodmodc  12200  fprodcnv  12247  demoivre  12395  demoivreALT  12396  nndivides  12419  0dvds  12433  muldvds1  12438  muldvds2  12439  dvdssubr  12461  dvdsadd2b  12462  odd2np1  12495  mulsucdiv2z  12507  ltoddhalfle  12515  ndvdssub  12552  gcdcom  12605  neggcd  12615  gcdabs2  12622  modgcd  12623  bezoutlemaz  12635  dfgcd2  12646  lcmcom  12697  neglcm  12708  lcmgcdeq  12716  coprmdvds  12725  qredeq  12729  divgcdcoprmex  12735  isprm3  12751  prmind2  12753  dvdsprm  12770  cncongrprm  12790  sqrt2irr  12795  hashgcdeq  12873  modprmn0modprm0  12890  coprimeprodsq  12891  pythagtriplem1  12899  pythagtriplem4  12902  pc2dvds  12964  pc11  12965  pcz  12966  pcprod  12980  prmunb  12996  1arithlem2  12998  1arithlem3  12999  1arith  13001  ptex  13408  issubmnd  13586  submcl  13623  resmhm2b  13633  grpinvsub  13726  dfgrp3mlem  13742  imasabl  13984  mgpress  14006  srgmulgass  14064  dfrhm2  14230  isrim0  14237  rmodislmodlem  14426  rmodislmod  14427  cnfldexp  14653  dvdsrzring  14679  znf1o  14727  eltg  14843  eltg2  14844  tgss  14854  tgss2  14870  basgen2  14872  bastop1  14874  opnneiss  14949  cnrest  15026  txss12  15057  hmeofvalg  15094  txswaphmeolem  15111  txswaphmeo  15112  blpnfctr  15230  metequiv  15286  metcnp3  15302  qtopbasss  15312  reopnap  15337  bl2ioo  15341  ioo2bl  15342  ioo2blex  15343  cncfval  15363  divccncfap  15381  addccncf  15391  expcncf  15400  dvexp  15502  dvmptfsum  15516  dvef  15518  efle  15567  reapef  15569  ptolemy  15615  logleb  15666  lgsprme0  15841  gausslemma2dlem1a  15857  gausslemma2dlem4  15863  lgsquadlem3  15878  2lgsoddprmlem2  15905  upgrpredgv  16067  uhgr2edg  16127  issubgr  16178  subgrprop  16180  subuhgr  16193  subupgr  16194  subumgr  16195  subusgr  16196  upgriswlkdc  16281  upgrwlkvtxedg  16285  g0wlk0  16291  clwwlkn1  16339  clwwlknonex2lem2  16359  uzdcinzz  16496  exmidsbthrlem  16730  triap  16741