Theorem ancoms 266

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 115	. 2 ⊢ (𝜓 → (𝜑 → 𝜒))
3	2	imp 123	1 ⊢ ((𝜓 ∧ 𝜑) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  adantl  273  syl2anr  286  anim12ci  335  sylan9bbr  456  anabss4  549  anabsi7  553  anabsi8  554  im2anan9r  571  bi2anan9r  579  syl3anr2  1252  mp3anr1  1295  mp3anr2  1296  mp3anr3  1297  eu5  2022  2exeu  2067  eqeqan12rd  2131  sylan9eqr  2169  r19.29vva  2551  morex  2837  sylan9ssr  3077  riinm  3851  breqan12rd  3911  elnn  4479  soinxp  4569  seinxp  4570  brelrng  4730  dminss  4911  imainss  4912  funsng  5127  funcnvuni  5150  f1co  5298  f1ocnv  5336  fun11iun  5344  funimass4  5426  fndmdifcom  5480  fsn2  5548  fvtp2g  5583  fvtp3g  5584  fvtp2  5586  fvtp3  5587  acexmid  5727  oveqan12rd  5748  cofunex2g  5964  brtposg  6105  tposoprab  6131  smores3  6144  smores2  6145  smoel  6151  tfri3  6218  rdgtfr  6225  rdgruledefgg  6226  omcl  6311  oeicl  6312  nnmsucr  6338  nnmcom  6339  nndir  6340  nnaordi  6358  nnaordr  6360  nnaword  6361  nnmordi  6366  nnaordex  6377  nnm00  6379  ersym  6395  elecg  6421  riinerm  6456  ecopovsym  6479  ecopovsymg  6482  ecovcom  6490  ecovicom  6491  mapvalg  6506  pmvalg  6507  elpmg  6512  elmapssres  6521  pmss12g  6523  ixpconstg  6555  ener  6627  domtr  6633  f1imaeng  6640  fundmen  6654  xpcomco  6673  xpsnen2g  6676  xpdom2  6678  xpdom1g  6680  enen2  6688  domen2  6690  ssfilem  6722  diffitest  6734  fiintim  6770  fundmfibi  6779  cnvti  6858  djuex  6880  nnnninf  6973  ltsopi  7076  pitric  7077  pitri3or  7078  addcompig  7085  mulcompig  7087  ltapig  7094  ltmpig  7095  nnppipi  7099  addcomnqg  7137  addassnqg  7138  distrnqg  7143  recexnq  7146  nqtri3or  7152  ltmnqg  7157  lt2addnq  7160  lt2mulnq  7161  ltbtwnnqq  7171  prarloclemarch2  7175  enq0ref  7189  distrnq0  7215  mulcomnq0  7216  prcdnql  7240  prcunqu  7241  prarloclemlt  7249  genpassl  7280  genpassu  7281  nqprloc  7301  nqpru  7308  appdiv0nq  7320  addcomprg  7334  mulcomprg  7336  distrlem4prl  7340  distrlem4pru  7341  1idprl  7346  1idpru  7347  ltsopr  7352  recexprlemss1l  7391  recexprlemss1u  7392  gt0srpr  7491  mulcomsrg  7500  ltsosr  7507  aptisr  7521  mulextsr1  7523  axaddcom  7605  axltwlin  7756  axapti  7759  letri3  7768  mul31  7816  cnegexlem3  7862  subval  7877  subcl  7884  pncan2  7892  pncan3  7893  npcan  7894  addsubeq4  7900  npncan3  7923  negsubdi2  7944  muladd  8065  subdi  8066  mulneg2  8077  mulsub  8082  ltleadd  8127  ltsubpos  8135  posdif  8136  addge01  8153  lesub0  8160  reapneg  8277  prodgt02  8521  prodge02  8523  ltdivmul  8544  lerec  8552  lediv2a  8563  le2msq  8569  msq11  8570  lbreu  8613  dfinfre  8624  creur  8627  creui  8628  cju  8629  nnmulcl  8651  nndivtr  8672  avgle1  8864  avgle2  8865  nn0nnaddcl  8912  zletric  9002  zrevaddcl  9008  znnsub  9009  znn0sub  9023  zdclt  9032  zextlt  9047  gtndiv  9050  prime  9054  peano5uzti  9063  uztrn2  9245  uztric  9249  uz11  9250  nn0pzuz  9284  indstr  9290  supinfneg  9292  infsupneg  9293  eluzdc  9306  qrevaddcl  9338  difrp  9379  xrltnsym  9472  xrltso  9475  xrlttri3  9476  xrletri3  9481  xleneg  9513  xaddcom  9537  xposdif  9558  ixxssixx  9578  iccid  9601  iooshf  9628  iccsupr  9642  iooneg  9664  iccneg  9665  fztri3or  9712  fzdcel  9713  fzn  9715  fzen  9716  fzass4  9735  fzrev  9757  fznn  9762  elfzp1b  9770  elfzm1b  9771  fz0fzdiffz0  9800  difelfznle  9805  fzon  9836  fzonmapblen  9857  eluzgtdifelfzo  9867  ubmelm1fzo  9896  subfzo0  9912  qletric  9914  ioo0  9930  ico0  9932  ioc0  9933  flqbi  9956  flqbi2  9957  flqzadd  9964  modfzo0difsn  10061  fzfig  10096  expcllem  10197  expap0  10216  mulbinom2  10301  expnbnd  10308  sq11ap  10351  hashfacen  10472  shftlem  10481  shftuz  10482  shftfvalg  10483  ovshftex  10484  shftfval  10486  shftval4  10493  shftval5  10494  2shfti  10496  mulreap  10529  sqrt11ap  10702  abs3dif  10769  abs2difabs  10772  maxabslemval  10872  maxle2  10876  maxclpr  10886  2zsupmax  10889  xrmaxiflemval  10911  xrmax2sup  10915  iooinsup  10938  climshftlemg  10963  fsumcnv  11098  explecnv  11166  geo2lim  11177  efler  11256  demoivre  11329  demoivreALT  11330  nndivides  11348  0dvds  11361  muldvds1  11366  muldvds2  11367  dvdssubr  11387  dvdsadd2b  11388  odd2np1  11418  mulsucdiv2z  11430  ltoddhalfle  11438  ndvdssub  11475  gcdcom  11510  neggcd  11519  gcdabs2  11526  modgcd  11527  bezoutlemaz  11537  dfgcd2  11548  lcmcom  11591  neglcm  11602  lcmgcdeq  11610  coprmdvds  11619  qredeq  11623  divgcdcoprmex  11629  isprm3  11645  prmind2  11647  dvdsprm  11663  cncongrprm  11681  sqrt2irr  11686  hashgcdeq  11749  eltg  12064  eltg2  12065  tgss  12075  tgss2  12091  basgen2  12093  bastop1  12095  opnneiss  12170  cnrest  12246  txss12  12277  blpnfctr  12428  metequiv  12484  metcnp3  12500  qtopbasss  12510  bl2ioo  12528  ioo2bl  12529  ioo2blex  12530  cncfval  12545  divccncfap  12563  addccncf  12572  expcncf  12578  uzdcinzz  12697  exmidsbthrlem  12909  triap  12916