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  4147  elnn  4753  soinxp  4845  seinxp  4846  brelrng  5013  dminss  5202  imainss  5203  funsng  5427  funcnvuni  5450  f1co  5610  f1ocnv  5652  fun11iun  5660  funimass4  5753  fndmdifcom  5815  fsn2  5882  fvtp2g  5924  fvtp3g  5925  fvtp2  5927  fvtp3  5928  riotaeqimp  6063  acexmid  6084  oveqan12rd  6105  cofunex2g  6339  brtposg  6525  tposoprab  6551  smores3  6564  smores2  6565  smoel  6571  tfri3  6638  rdgtfr  6645  rdgruledefgg  6646  omcl  6734  oeicl  6735  nnmsucr  6761  nnmcom  6762  nndir  6763  nnaordi  6781  nnaordr  6783  nnaword  6784  nnmordi  6789  nnaordex  6801  nnm00  6803  ersym  6819  elecg  6847  riinerm  6882  ecopovsym  6905  ecopovsymg  6908  ecovcom  6916  ecovicom  6917  mapvalg  6932  pmvalg  6933  elpmg  6938  elmapssres  6954  pmss12g  6956  ixpconstg  6989  domssr  7064  ener  7066  domtr  7072  f1imaeng  7079  fundmen  7094  xpcomco  7124  xpsnen2g  7127  xpdom2  7129  xpdom1g  7131  enen2  7141  domen2  7143  ssfilem  7177  ssfilemd  7179  diffitest  7191  fiintim  7238  fundmfibi  7252  f1setfi  7317  cnvti  7360  djuex  7384  nnnninf  7467  netap  7621  2omotaplemap  7624  ltsopi  7688  pitric  7689  pitri3or  7690  addcompig  7697  mulcompig  7699  ltapig  7706  ltmpig  7707  nnppipi  7711  addcomnqg  7749  addassnqg  7750  distrnqg  7755  recexnq  7758  nqtri3or  7764  ltmnqg  7769  lt2addnq  7772  lt2mulnq  7773  ltbtwnnqq  7783  prarloclemarch2  7787  enq0ref  7801  distrnq0  7827  mulcomnq0  7828  prcdnql  7852  prcunqu  7853  prarloclemlt  7861  genpassl  7892  genpassu  7893  nqprloc  7913  nqpru  7920  appdiv0nq  7932  addcomprg  7946  mulcomprg  7948  distrlem4prl  7952  distrlem4pru  7953  1idprl  7958  1idpru  7959  ltsopr  7964  recexprlemss1l  8003  recexprlemss1u  8004  gt0srpr  8116  mulcomsrg  8125  ltsosr  8132  aptisr  8147  mulextsr1  8149  map2psrprg  8173  axaddcom  8238  axltwlin  8394  axapti  8397  letri3  8407  eqlelt  8413  mul31  8459  cnegexlem3  8505  subval  8520  subcl  8527  pncan2  8535  pncan3  8536  npcan  8537  addsubeq4  8543  npncan3  8566  negsubdi2  8587  muladd  8713  subdi  8714  mulneg2  8725  mulsub  8730  ltleadd  8776  ltsubpos  8784  posdif  8785  addge01  8802  lesub0  8809  reapneg  8928  prodgt02  9186  prodge02  9188  ltdivmul  9209  lerec  9217  lediv2a  9228  le2msq  9234  msq11  9235  lbreu  9278  dfinfre  9289  creur  9292  creui  9293  cju  9294  indval  9299  nnmulcl  9328  nndivtr  9349  avgle1  9551  avgle2  9552  nn0nnaddcl  9599  zletric  9693  zrevaddcl  9700  znnsub  9701  znn0sub  9715  ltsubnn0  9717  zdclt  9727  zextlt  9743  gtndiv  9746  prime  9750  peano5uzti  9759  uztrn2  9950  uztric  9954  uz11  9955  nn0pzuz  9997  indstr  10003  supinfneg  10005  infsupneg  10006  eluzdc  10020  qrevaddcl  10054  difrp  10104  xrltnsym  10206  xrltso  10209  xrlttri3  10210  xrletri3  10217  xleneg  10250  xaddcom  10274  xposdif  10295  ixxssixx  10315  iccid  10338  iooshf  10365  iccsupr  10379  iooneg  10401  iccneg  10402  fztri3or  10454  fzdcel  10455  fzn  10457  fzen  10458  fzass4  10479  fzrev  10502  fznn  10507  elfzp1b  10515  elfzm1b  10516  fz0fzdiffz0  10548  difelfznle  10553  fzon  10585  fzo0n  10586  fzonmapblen  10610  elfzoextl  10620  eluzgtdifelfzo  10626  ubmelm1fzo  10655  subfzo0  10672  qletric  10687  qdclt  10691  qdcle  10692  ioo0  10705  ico0  10707  ioc0  10708  flqbi  10739  flqbi2  10740  flqzadd  10747  modfzo0difsn  10846  fzfig  10881  expcllem  11001  expap0  11020  mulbinom2  11107  expnbnd  11115  sq11ap  11159  hashfacen  11299  iswrdinn0  11324  ccatsymb  11385  ccatalpha  11396  swrd0g  11447  swrdsbslen  11453  swrdspsleq  11454  wrd2ind  11510  pfxccatin12lem1  11515  pfxccatin12lem2  11518  pfxccatin12  11520  swrdccat3blem  11526  shftlem  11596  shftuz  11597  shftfvalg  11598  ovshftex  11599  shftfval  11601  shftval4  11608  shftval5  11609  2shfti  11611  mulreap  11644  sqrt11ap  11819  abs3dif  11887  abs2difabs  11890  maxabslemval  11990  maxle2  11994  maxclpr  12004  2zsupmax  12008  mingeb  12026  2zinfmin  12027  xrmaxiflemval  12034  xrmax2sup  12038  iooinsup  12061  climshftlemg  12086  fsumcnv  12222  explecnv  12290  geo2lim  12301  prodmodc  12363  fprodcnv  12410  demoivre  12558  demoivreALT  12559  nndivides  12582  0dvds  12596  muldvds1  12601  muldvds2  12602  dvdssubr  12624  dvdsadd2b  12625  odd2np1  12658  mulsucdiv2z  12670  ltoddhalfle  12678  ndvdssub  12715  gcdcom  12768  neggcd  12778  gcdabs2  12785  modgcd  12786  bezoutlemaz  12798  dfgcd2  12809  lcmcom  12860  neglcm  12871  lcmgcdeq  12879  coprmdvds  12888  qredeq  12892  divgcdcoprmex  12898  isprm3  12914  prmind2  12916  dvdsprm  12934  cncongrprm  12954  sqrt2irr  12959  nnmaxpw  12971  hashgcdeq  13040  modprmn0modprm0  13057  coprimeprodsq  13058  pythagtriplem1  13066  pythagtriplem4  13069  pc2dvds  13131  pc11  13132  pcz  13133  pcprod  13147  prmunb  13163  1arithlem2  13165  1arithlem3  13166  1arith  13168  ptex  13669  issubmnd  13806  submcl  13837  resmhm2b  13847  grpinvsub  13938  dfgrp3mlem  13954  imasabl  14191  mgpress  14281  srgmulgass  14344  dfrhm2  14512  isrim0  14519  rmodislmodlem  14738  rmodislmod  14739  cnfldexp  14965  dvdsrzring  14989  znf1o  15037  eltg  15205  eltg2  15206  tgss  15216  tgss2  15232  basgen2  15234  bastop1  15236  opnneiss  15311  cnrest  15388  txss12  15419  hmeofvalg  15456  txswaphmeolem  15473  txswaphmeo  15474  blpnfctr  15592  metequiv  15648  metcnp3  15664  qtopbasss  15674  reopnap  15699  bl2ioo  15703  ioo2bl  15704  ioo2blex  15705  cncfval  15725  divccncfap  15743  addccncf  15753  expcncf  15762  dvexp  15864  dvmptfsum  15878  dvef  15880  efle  15929  reapef  15931  ptolemy  15978  logleb  16030  logdivle  16050  lgsprme0  16283  gausslemma2dlem1a  16299  gausslemma2dlem4  16305  lgsquadlem3  16320  2lgsoddprmlem2  16347  upgrpredgv  16509  uhgr2edg  16569  issubgr  16620  subgrprop  16622  subuhgr  16635  subupgr  16636  subumgr  16637  subusgr  16638  upgriswlkdc  16723  upgrwlkvtxedg  16727  g0wlk0  16733  clwwlkn1  16781  clwwlknonex2lem2  16801  dichmul0orlem3  16877  uzdcinzz  16948  exmidsbthrlem  17189  triap  17200