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 ⊢ ((𝜓 ∧ 𝜑) → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  adantl  277  syl2anr  290  anim12ci  339  sylan9bbr  467  anabss4  583  anabsi7  587  anabsi8  588  im2anan9r  607  bi2anan9r  615  syl3anr2  1331  mp3anr1  1375  mp3anr2  1376  mp3anr3  1377  stoic1b  1477  cbvaldvaw  1986  eu5  2134  2exeu  2179  eqeqan12rd  2255  sylan9eqr  2293  r19.29vva  2696  morex  3010  sylan9ssr  3262  riinm  4085  breqan12rd  4148  elnn  4755  soinxp  4847  seinxp  4848  brelrng  5015  dminss  5205  imainss  5206  funsng  5430  funcnvuni  5453  f1co  5613  f1ocnv  5655  fun11iun  5663  funimass4  5756  fndmdifcom  5818  fsn2  5885  fvtp2g  5927  fvtp3g  5928  fvtp2  5930  fvtp3  5931  riotaeqimp  6066  acexmid  6087  oveqan12rd  6108  cofunex2g  6343  brtposg  6529  tposoprab  6555  smores3  6568  smores2  6569  smoel  6575  tfri3  6642  rdgtfr  6649  rdgruledefgg  6650  omcl  6738  oeicl  6739  nnmsucr  6765  nnmcom  6766  nndir  6767  nnaordi  6785  nnaordr  6787  nnaword  6788  nnmordi  6793  nnaordex  6805  nnm00  6807  ersym  6823  elecg  6851  riinerm  6886  ecopovsym  6909  ecopovsymg  6912  ecovcom  6920  ecovicom  6921  mapvalg  6936  pmvalg  6937  elpmg  6942  elmapssres  6958  pmss12g  6960  ixpconstg  6994  domssr  7069  ener  7071  domtr  7077  f1imaeng  7084  fundmen  7099  xpcomco  7129  xpsnen2g  7132  xpdom2  7134  xpdom1g  7136  enen2  7146  domen2  7148  ssfilem  7182  ssfilemd  7184  diffitest  7196  fiintim  7243  fundmfibi  7257  f1setfi  7323  cnvti  7366  djuex  7390  nnnninf  7473  netap  7627  2omotaplemap  7630  ltsopi  7694  pitric  7695  pitri3or  7696  addcompig  7703  mulcompig  7705  ltapig  7712  ltmpig  7713  nnppipi  7717  addcomnqg  7755  addassnqg  7756  distrnqg  7761  recexnq  7764  nqtri3or  7770  ltmnqg  7775  lt2addnq  7778  lt2mulnq  7779  ltbtwnnqq  7789  prarloclemarch2  7793  enq0ref  7807  distrnq0  7833  mulcomnq0  7834  prcdnql  7858  prcunqu  7859  prarloclemlt  7867  genpassl  7898  genpassu  7899  nqprloc  7919  nqpru  7926  appdiv0nq  7938  addcomprg  7952  mulcomprg  7954  distrlem4prl  7958  distrlem4pru  7959  1idprl  7964  1idpru  7965  ltsopr  7970  recexprlemss1l  8009  recexprlemss1u  8010  gt0srpr  8122  mulcomsrg  8131  ltsosr  8138  aptisr  8153  mulextsr1  8155  map2psrprg  8179  axaddcom  8244  axltwlin  8400  axapti  8403  letri3  8413  eqlelt  8419  mul31  8465  cnegexlem3  8511  subval  8526  subcl  8533  pncan2  8541  pncan3  8542  npcan  8543  addsubeq4  8549  npncan3  8572  negsubdi2  8593  muladd  8719  subdi  8720  mulneg2  8731  mulsub  8736  ltleadd  8782  ltsubpos  8790  posdif  8791  addge01  8808  lesub0  8815  reapneg  8934  prodgt02  9192  prodge02  9194  ltdivmul  9215  lerec  9223  lediv2a  9234  le2msq  9240  msq11  9241  lbreu  9284  dfinfre  9295  creur  9298  creui  9299  cju  9300  indval  9306  nnmulcl  9335  nndivtr  9356  avgle1  9558  avgle2  9559  nn0nnaddcl  9606  zletric  9700  zrevaddcl  9707  znnsub  9708  znn0sub  9722  ltsubnn0  9724  zdclt  9734  zextlt  9750  gtndiv  9753  prime  9757  peano5uzti  9766  uztrn2  9957  uztric  9961  uz11  9962  nn0pzuz  10004  indstr  10010  supinfneg  10012  infsupneg  10013  eluzdc  10027  qrevaddcl  10061  difrp  10111  xrltnsym  10213  xrltso  10216  xrlttri3  10217  xrletri3  10224  xleneg  10257  xaddcom  10281  xposdif  10302  ixxssixx  10322  iccid  10345  iooshf  10372  iccsupr  10386  iooneg  10408  iccneg  10409  fztri3or  10461  fzdcel  10462  fzn  10464  fzen  10465  fzass4  10486  fzrev  10509  fznn  10514  elfzp1b  10522  elfzm1b  10523  fz0fzdiffz0  10555  difelfznle  10560  fzon  10592  fzo0n  10593  fzonmapblen  10617  elfzoextl  10627  eluzgtdifelfzo  10633  ubmelm1fzo  10662  subfzo0  10679  qletric  10694  qdclt  10698  qdcle  10699  ioo0  10712  ico0  10714  ioc0  10715  flqbi  10747  flqbi2  10748  flqzadd  10755  modfzo0difsn  10854  fzfig  10889  expcllem  11009  expap0  11028  mulbinom2  11115  expnbnd  11123  sq11ap  11167  hashfacen  11307  iswrdinn0  11332  ccatsymb  11393  ccatalpha  11404  swrd0g  11455  swrdsbslen  11461  swrdspsleq  11462  wrd2ind  11518  pfxccatin12lem1  11523  pfxccatin12lem2  11526  pfxccatin12  11528  swrdccat3blem  11534  shftlem  11604  shftuz  11605  shftfvalg  11606  ovshftex  11607  shftfval  11609  shftval4  11616  shftval5  11617  2shfti  11619  mulreap  11652  sqrt11ap  11827  abs3dif  11895  abs2difabs  11898  maxabslemval  11998  maxle2  12002  maxclpr  12012  2zsupmax  12016  mingeb  12034  2zinfmin  12035  xrmaxiflemval  12042  xrmax2sup  12046  iooinsup  12069  climshftlemg  12094  fsumcnv  12230  explecnv  12298  geo2lim  12309  prodmodc  12371  fprodcnv  12418  demoivre  12566  demoivreALT  12567  nndivides  12590  0dvds  12604  muldvds1  12609  muldvds2  12610  dvdssubr  12632  dvdsadd2b  12633  odd2np1  12666  mulsucdiv2z  12678  ltoddhalfle  12686  ndvdssub  12723  gcdcom  12776  neggcd  12786  gcdabs2  12793  modgcd  12794  bezoutlemaz  12806  dfgcd2  12817  lcmcom  12868  neglcm  12879  lcmgcdeq  12887  coprmdvds  12896  qredeq  12900  divgcdcoprmex  12906  isprm3  12922  prmind2  12924  dvdsprm  12942  cncongrprm  12962  sqrt2irr  12967  nnmaxpw  12979  hashgcdeq  13048  modprmn0modprm0  13065  coprimeprodsq  13066  pythagtriplem1  13074  pythagtriplem4  13077  pc2dvds  13139  pc11  13140  pcz  13141  pcprod  13155  prmunb  13171  1arithlem2  13173  1arithlem3  13174  1arith  13176  ptex  13678  issubmnd  13815  submcl  13846  resmhm2b  13856  grpinvsub  13947  dfgrp3mlem  13963  cntz2ss  14169  cntzrec  14170  imasabl  14231  mgpress  14338  srgmulgass  14401  dfrhm2  14571  isrim0  14578  rmodislmodlem  14797  rmodislmod  14798  cnfldexp  15024  dvdsrzring  15048  znf1o  15096  eltg  15290  eltg2  15291  tgss  15301  tgss2  15317  basgen2  15319  bastop1  15321  opnneiss  15396  cnrest  15473  txss12  15504  hmeofvalg  15541  txswaphmeolem  15558  txswaphmeo  15559  blpnfctr  15677  metequiv  15733  metcnp3  15749  qtopbasss  15759  reopnap  15784  bl2ioo  15788  ioo2bl  15789  ioo2blex  15790  cncfval  15810  divccncfap  15828  addccncf  15838  expcncf  15847  dvexp  15949  dvmptfsum  15963  dvef  15965  efle  16014  reapef  16016  ptolemy  16063  logleb  16117  logdivle  16137  lgsprme0  16378  gausslemma2dlem1a  16394  gausslemma2dlem4  16400  lgsquadlem3  16415  2lgsoddprmlem2  16442  upgrpredgv  16604  uhgr2edg  16664  issubgr  16715  subgrprop  16717  subuhgr  16730  subupgr  16731  subumgr  16732  subusgr  16733  upgriswlkdc  16818  upgrwlkvtxedg  16822  g0wlk0  16828  clwwlkn1  16876  clwwlknonex2lem2  16896  dichmul0orlem3  16972  uzdcinzz  17043  exmidsbthrlem  17285  triap  17296