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  1982  eu5  2130  2exeu  2175  eqeqan12rd  2251  sylan9eqr  2289  r19.29vva  2690  morex  3004  sylan9ssr  3256  riinm  4069  breqan12rd  4131  elnn  4733  soinxp  4825  seinxp  4826  brelrng  4993  dminss  5182  imainss  5183  funsng  5407  funcnvuni  5430  f1co  5590  f1ocnv  5632  fun11iun  5640  funimass4  5732  fndmdifcom  5789  fsn2  5856  fvtp2g  5898  fvtp3g  5899  fvtp2  5901  fvtp3  5902  riotaeqimp  6036  acexmid  6057  oveqan12rd  6078  cofunex2g  6312  brtposg  6498  tposoprab  6524  smores3  6537  smores2  6538  smoel  6544  tfri3  6611  rdgtfr  6618  rdgruledefgg  6619  omcl  6707  oeicl  6708  nnmsucr  6734  nnmcom  6735  nndir  6736  nnaordi  6754  nnaordr  6756  nnaword  6757  nnmordi  6762  nnaordex  6774  nnm00  6776  ersym  6792  elecg  6820  riinerm  6855  ecopovsym  6878  ecopovsymg  6881  ecovcom  6889  ecovicom  6890  mapvalg  6905  pmvalg  6906  elpmg  6911  elmapssres  6920  pmss12g  6922  ixpconstg  6955  domssr  7030  ener  7032  domtr  7038  f1imaeng  7045  fundmen  7060  xpcomco  7090  xpsnen2g  7093  xpdom2  7095  xpdom1g  7097  enen2  7107  domen2  7109  ssfilem  7143  ssfilemd  7145  diffitest  7157  fiintim  7204  fundmfibi  7218  cnvti  7323  djuex  7347  nnnninf  7430  netap  7584  2omotaplemap  7587  ltsopi  7651  pitric  7652  pitri3or  7653  addcompig  7660  mulcompig  7662  ltapig  7669  ltmpig  7670  nnppipi  7674  addcomnqg  7712  addassnqg  7713  distrnqg  7718  recexnq  7721  nqtri3or  7727  ltmnqg  7732  lt2addnq  7735  lt2mulnq  7736  ltbtwnnqq  7746  prarloclemarch2  7750  enq0ref  7764  distrnq0  7790  mulcomnq0  7791  prcdnql  7815  prcunqu  7816  prarloclemlt  7824  genpassl  7855  genpassu  7856  nqprloc  7876  nqpru  7883  appdiv0nq  7895  addcomprg  7909  mulcomprg  7911  distrlem4prl  7915  distrlem4pru  7916  1idprl  7921  1idpru  7922  ltsopr  7927  recexprlemss1l  7966  recexprlemss1u  7967  gt0srpr  8079  mulcomsrg  8088  ltsosr  8095  aptisr  8110  mulextsr1  8112  map2psrprg  8136  axaddcom  8201  axltwlin  8357  axapti  8360  letri3  8370  eqlelt  8376  mul31  8420  cnegexlem3  8466  subval  8481  subcl  8488  pncan2  8496  pncan3  8497  npcan  8498  addsubeq4  8504  npncan3  8527  negsubdi2  8548  muladd  8674  subdi  8675  mulneg2  8686  mulsub  8691  ltleadd  8737  ltsubpos  8745  posdif  8746  addge01  8763  lesub0  8770  reapneg  8888  prodgt02  9144  prodge02  9146  ltdivmul  9167  lerec  9175  lediv2a  9186  le2msq  9192  msq11  9193  lbreu  9236  dfinfre  9247  creur  9250  creui  9251  cju  9252  nnmulcl  9275  nndivtr  9296  avgle1  9496  avgle2  9497  nn0nnaddcl  9544  zletric  9638  zrevaddcl  9645  znnsub  9646  znn0sub  9660  ltsubnn0  9662  zdclt  9672  zextlt  9688  gtndiv  9691  prime  9695  peano5uzti  9704  uztrn2  9890  uztric  9894  uz11  9895  nn0pzuz  9937  indstr  9943  supinfneg  9945  infsupneg  9946  eluzdc  9960  qrevaddcl  9994  difrp  10043  xrltnsym  10145  xrltso  10148  xrlttri3  10149  xrletri3  10156  xleneg  10189  xaddcom  10213  xposdif  10234  ixxssixx  10254  iccid  10277  iooshf  10304  iccsupr  10318  iooneg  10340  iccneg  10341  fztri3or  10393  fzdcel  10394  fzn  10396  fzen  10397  fzass4  10417  fzrev  10440  fznn  10445  elfzp1b  10453  elfzm1b  10454  fz0fzdiffz0  10486  difelfznle  10491  fzon  10523  fzo0n  10524  fzonmapblen  10548  elfzoextl  10558  eluzgtdifelfzo  10564  ubmelm1fzo  10593  subfzo0  10610  qletric  10625  qdclt  10629  qdcle  10630  ioo0  10643  ico0  10645  ioc0  10646  flqbi  10674  flqbi2  10675  flqzadd  10682  modfzo0difsn  10781  fzfig  10816  expcllem  10936  expap0  10955  mulbinom2  11042  expnbnd  11050  sq11ap  11094  hashfacen  11233  iswrdinn0  11254  ccatsymb  11315  ccatalpha  11326  swrd0g  11377  swrdsbslen  11383  swrdspsleq  11384  wrd2ind  11440  pfxccatin12lem1  11445  pfxccatin12lem2  11448  pfxccatin12  11450  swrdccat3blem  11456  shftlem  11526  shftuz  11527  shftfvalg  11528  ovshftex  11529  shftfval  11531  shftval4  11538  shftval5  11539  2shfti  11541  mulreap  11574  sqrt11ap  11748  abs3dif  11815  abs2difabs  11818  maxabslemval  11918  maxle2  11922  maxclpr  11932  2zsupmax  11936  mingeb  11952  2zinfmin  11953  xrmaxiflemval  11960  xrmax2sup  11964  iooinsup  11987  climshftlemg  12012  fsumcnv  12148  explecnv  12216  geo2lim  12227  prodmodc  12289  fprodcnv  12336  demoivre  12484  demoivreALT  12485  nndivides  12508  0dvds  12522  muldvds1  12527  muldvds2  12528  dvdssubr  12550  dvdsadd2b  12551  odd2np1  12584  mulsucdiv2z  12596  ltoddhalfle  12604  ndvdssub  12641  gcdcom  12694  neggcd  12704  gcdabs2  12711  modgcd  12712  bezoutlemaz  12724  dfgcd2  12735  lcmcom  12786  neglcm  12797  lcmgcdeq  12805  coprmdvds  12814  qredeq  12818  divgcdcoprmex  12824  isprm3  12840  prmind2  12842  dvdsprm  12859  cncongrprm  12879  sqrt2irr  12884  hashgcdeq  12962  modprmn0modprm0  12979  coprimeprodsq  12980  pythagtriplem1  12988  pythagtriplem4  12991  pc2dvds  13053  pc11  13054  pcz  13055  pcprod  13069  prmunb  13085  1arithlem2  13087  1arithlem3  13088  1arith  13090  ptex  13561  issubmnd  13739  submcl  13776  resmhm2b  13786  grpinvsub  13879  dfgrp3mlem  13895  imasabl  14137  mgpress  14159  srgmulgass  14217  dfrhm2  14384  isrim0  14391  rmodislmodlem  14610  rmodislmod  14611  cnfldexp  14837  dvdsrzring  14863  znf1o  14911  eltg  15029  eltg2  15030  tgss  15040  tgss2  15056  basgen2  15058  bastop1  15060  opnneiss  15135  cnrest  15212  txss12  15243  hmeofvalg  15280  txswaphmeolem  15297  txswaphmeo  15298  blpnfctr  15416  metequiv  15472  metcnp3  15488  qtopbasss  15498  reopnap  15523  bl2ioo  15527  ioo2bl  15528  ioo2blex  15529  cncfval  15549  divccncfap  15567  addccncf  15577  expcncf  15586  dvexp  15688  dvmptfsum  15702  dvef  15704  efle  15753  reapef  15755  ptolemy  15801  logleb  15852  lgsprme0  16027  gausslemma2dlem1a  16043  gausslemma2dlem4  16049  lgsquadlem3  16064  2lgsoddprmlem2  16091  upgrpredgv  16253  uhgr2edg  16313  issubgr  16364  subgrprop  16366  subuhgr  16379  subupgr  16380  subumgr  16381  subusgr  16382  upgriswlkdc  16467  upgrwlkvtxedg  16471  g0wlk0  16477  clwwlkn1  16525  clwwlknonex2lem2  16545  uzdcinzz  16682  exmidsbthrlem  16914  triap  16925