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  577  anabsi7  581  anabsi8  582  im2anan9r  599  bi2anan9r  607  syl3anr2  1302  mp3anr1  1345  mp3anr2  1346  mp3anr3  1347  stoic1b  1439  cbvaldvaw  1942  eu5  2089  2exeu  2134  eqeqan12rd  2210  sylan9eqr  2248  r19.29vva  2639  morex  2945  sylan9ssr  3194  riinm  3986  breqan12rd  4047  elnn  4639  soinxp  4730  seinxp  4731  brelrng  4894  dminss  5081  imainss  5082  funsng  5301  funcnvuni  5324  f1co  5472  f1ocnv  5514  fun11iun  5522  funimass4  5608  fndmdifcom  5665  fsn2  5733  fvtp2g  5768  fvtp3g  5769  fvtp2  5771  fvtp3  5772  acexmid  5918  oveqan12rd  5939  cofunex2g  6164  brtposg  6309  tposoprab  6335  smores3  6348  smores2  6349  smoel  6355  tfri3  6422  rdgtfr  6429  rdgruledefgg  6430  omcl  6516  oeicl  6517  nnmsucr  6543  nnmcom  6544  nndir  6545  nnaordi  6563  nnaordr  6565  nnaword  6566  nnmordi  6571  nnaordex  6583  nnm00  6585  ersym  6601  elecg  6629  riinerm  6664  ecopovsym  6687  ecopovsymg  6690  ecovcom  6698  ecovicom  6699  mapvalg  6714  pmvalg  6715  elpmg  6720  elmapssres  6729  pmss12g  6731  ixpconstg  6763  ener  6835  domtr  6841  f1imaeng  6848  fundmen  6862  xpcomco  6882  xpsnen2g  6885  xpdom2  6887  xpdom1g  6889  enen2  6899  domen2  6901  ssfilem  6933  diffitest  6945  fiintim  6987  fundmfibi  6999  cnvti  7080  djuex  7104  nnnninf  7187  netap  7316  2omotaplemap  7319  ltsopi  7382  pitric  7383  pitri3or  7384  addcompig  7391  mulcompig  7393  ltapig  7400  ltmpig  7401  nnppipi  7405  addcomnqg  7443  addassnqg  7444  distrnqg  7449  recexnq  7452  nqtri3or  7458  ltmnqg  7463  lt2addnq  7466  lt2mulnq  7467  ltbtwnnqq  7477  prarloclemarch2  7481  enq0ref  7495  distrnq0  7521  mulcomnq0  7522  prcdnql  7546  prcunqu  7547  prarloclemlt  7555  genpassl  7586  genpassu  7587  nqprloc  7607  nqpru  7614  appdiv0nq  7626  addcomprg  7640  mulcomprg  7642  distrlem4prl  7646  distrlem4pru  7647  1idprl  7652  1idpru  7653  ltsopr  7658  recexprlemss1l  7697  recexprlemss1u  7698  gt0srpr  7810  mulcomsrg  7819  ltsosr  7826  aptisr  7841  mulextsr1  7843  map2psrprg  7867  axaddcom  7932  axltwlin  8089  axapti  8092  letri3  8102  eqlelt  8108  mul31  8152  cnegexlem3  8198  subval  8213  subcl  8220  pncan2  8228  pncan3  8229  npcan  8230  addsubeq4  8236  npncan3  8259  negsubdi2  8280  muladd  8405  subdi  8406  mulneg2  8417  mulsub  8422  ltleadd  8467  ltsubpos  8475  posdif  8476  addge01  8493  lesub0  8500  reapneg  8618  prodgt02  8874  prodge02  8876  ltdivmul  8897  lerec  8905  lediv2a  8916  le2msq  8922  msq11  8923  lbreu  8966  dfinfre  8977  creur  8980  creui  8981  cju  8982  nnmulcl  9005  nndivtr  9026  avgle1  9226  avgle2  9227  nn0nnaddcl  9274  zletric  9364  zrevaddcl  9370  znnsub  9371  znn0sub  9385  ltsubnn0  9387  zdclt  9397  zextlt  9412  gtndiv  9415  prime  9419  peano5uzti  9428  uztrn2  9613  uztric  9617  uz11  9618  nn0pzuz  9655  indstr  9661  supinfneg  9663  infsupneg  9664  eluzdc  9678  qrevaddcl  9712  difrp  9761  xrltnsym  9862  xrltso  9865  xrlttri3  9866  xrletri3  9873  xleneg  9906  xaddcom  9930  xposdif  9951  ixxssixx  9971  iccid  9994  iooshf  10021  iccsupr  10035  iooneg  10057  iccneg  10058  fztri3or  10108  fzdcel  10109  fzn  10111  fzen  10112  fzass4  10131  fzrev  10153  fznn  10158  elfzp1b  10166  elfzm1b  10167  fz0fzdiffz0  10199  difelfznle  10204  fzon  10236  fzonmapblen  10257  eluzgtdifelfzo  10267  ubmelm1fzo  10296  subfzo0  10312  qletric  10314  qdclt  10318  ioo0  10331  ico0  10333  ioc0  10334  flqbi  10362  flqbi2  10363  flqzadd  10370  modfzo0difsn  10469  fzfig  10504  expcllem  10624  expap0  10643  mulbinom2  10730  expnbnd  10737  sq11ap  10781  hashfacen  10910  iswrdinn0  10922  shftlem  10963  shftuz  10964  shftfvalg  10965  ovshftex  10966  shftfval  10968  shftval4  10975  shftval5  10976  2shfti  10978  mulreap  11011  sqrt11ap  11185  abs3dif  11252  abs2difabs  11255  maxabslemval  11355  maxle2  11359  maxclpr  11369  2zsupmax  11372  mingeb  11388  2zinfmin  11389  xrmaxiflemval  11396  xrmax2sup  11400  iooinsup  11423  climshftlemg  11448  fsumcnv  11583  explecnv  11651  geo2lim  11662  prodmodc  11724  fprodcnv  11771  demoivre  11919  demoivreALT  11920  nndivides  11943  0dvds  11957  muldvds1  11962  muldvds2  11963  dvdssubr  11985  dvdsadd2b  11986  odd2np1  12017  mulsucdiv2z  12029  ltoddhalfle  12037  ndvdssub  12074  gcdcom  12113  neggcd  12123  gcdabs2  12130  modgcd  12131  bezoutlemaz  12143  dfgcd2  12154  lcmcom  12205  neglcm  12216  lcmgcdeq  12224  coprmdvds  12233  qredeq  12237  divgcdcoprmex  12243  isprm3  12259  prmind2  12261  dvdsprm  12278  cncongrprm  12298  sqrt2irr  12303  hashgcdeq  12380  modprmn0modprm0  12397  coprimeprodsq  12398  pythagtriplem1  12406  pythagtriplem4  12409  pc2dvds  12471  pc11  12472  pcz  12473  pcprod  12487  prmunb  12503  1arithlem2  12505  1arithlem3  12506  1arith  12508  ptex  12878  issubmnd  13026  submcl  13054  resmhm2b  13064  grpinvsub  13157  dfgrp3mlem  13173  imasabl  13409  mgpress  13430  srgmulgass  13488  dfrhm2  13653  isrim0  13660  rmodislmodlem  13849  rmodislmod  13850  cnfldexp  14076  dvdsrzring  14102  znf1o  14150  eltg  14231  eltg2  14232  tgss  14242  tgss2  14258  basgen2  14260  bastop1  14262  opnneiss  14337  cnrest  14414  txss12  14445  hmeofvalg  14482  txswaphmeolem  14499  txswaphmeo  14500  blpnfctr  14618  metequiv  14674  metcnp3  14690  qtopbasss  14700  reopnap  14725  bl2ioo  14729  ioo2bl  14730  ioo2blex  14731  cncfval  14751  divccncfap  14769  addccncf  14779  expcncf  14788  dvexp  14890  dvmptfsum  14904  dvef  14906  efle  14952  reapef  14954  ptolemy  15000  logleb  15051  lgsprme0  15199  gausslemma2dlem1a  15215  gausslemma2dlem4  15221  lgsquadlem3  15236  2lgsoddprmlem2  15263  uzdcinzz  15360  exmidsbthrlem  15582  triap  15589