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  7359  djuex  7383  nnnninf  7466  netap  7620  2omotaplemap  7623  ltsopi  7687  pitric  7688  pitri3or  7689  addcompig  7696  mulcompig  7698  ltapig  7705  ltmpig  7706  nnppipi  7710  addcomnqg  7748  addassnqg  7749  distrnqg  7754  recexnq  7757  nqtri3or  7763  ltmnqg  7768  lt2addnq  7771  lt2mulnq  7772  ltbtwnnqq  7782  prarloclemarch2  7786  enq0ref  7800  distrnq0  7826  mulcomnq0  7827  prcdnql  7851  prcunqu  7852  prarloclemlt  7860  genpassl  7891  genpassu  7892  nqprloc  7912  nqpru  7919  appdiv0nq  7931  addcomprg  7945  mulcomprg  7947  distrlem4prl  7951  distrlem4pru  7952  1idprl  7957  1idpru  7958  ltsopr  7963  recexprlemss1l  8002  recexprlemss1u  8003  gt0srpr  8115  mulcomsrg  8124  ltsosr  8131  aptisr  8146  mulextsr1  8148  map2psrprg  8172  axaddcom  8237  axltwlin  8393  axapti  8396  letri3  8406  eqlelt  8412  mul31  8457  cnegexlem3  8503  subval  8518  subcl  8525  pncan2  8533  pncan3  8534  npcan  8535  addsubeq4  8541  npncan3  8564  negsubdi2  8585  muladd  8711  subdi  8712  mulneg2  8723  mulsub  8728  ltleadd  8774  ltsubpos  8782  posdif  8783  addge01  8800  lesub0  8807  reapneg  8926  prodgt02  9184  prodge02  9186  ltdivmul  9207  lerec  9215  lediv2a  9226  le2msq  9232  msq11  9233  lbreu  9276  dfinfre  9287  creur  9290  creui  9291  cju  9292  indval  9297  nnmulcl  9326  nndivtr  9347  avgle1  9548  avgle2  9549  nn0nnaddcl  9596  zletric  9690  zrevaddcl  9697  znnsub  9698  znn0sub  9712  ltsubnn0  9714  zdclt  9724  zextlt  9740  gtndiv  9743  prime  9747  peano5uzti  9756  uztrn2  9942  uztric  9946  uz11  9947  nn0pzuz  9989  indstr  9995  supinfneg  9997  infsupneg  9998  eluzdc  10012  qrevaddcl  10046  difrp  10095  xrltnsym  10197  xrltso  10200  xrlttri3  10201  xrletri3  10208  xleneg  10241  xaddcom  10265  xposdif  10286  ixxssixx  10306  iccid  10329  iooshf  10356  iccsupr  10370  iooneg  10392  iccneg  10393  fztri3or  10445  fzdcel  10446  fzn  10448  fzen  10449  fzass4  10470  fzrev  10493  fznn  10498  elfzp1b  10506  elfzm1b  10507  fz0fzdiffz0  10539  difelfznle  10544  fzon  10576  fzo0n  10577  fzonmapblen  10601  elfzoextl  10611  eluzgtdifelfzo  10617  ubmelm1fzo  10646  subfzo0  10663  qletric  10678  qdclt  10682  qdcle  10683  ioo0  10696  ico0  10698  ioc0  10699  flqbi  10727  flqbi2  10728  flqzadd  10735  modfzo0difsn  10834  fzfig  10869  expcllem  10989  expap0  11008  mulbinom2  11095  expnbnd  11103  sq11ap  11147  hashfacen  11286  iswrdinn0  11311  ccatsymb  11372  ccatalpha  11383  swrd0g  11434  swrdsbslen  11440  swrdspsleq  11441  wrd2ind  11497  pfxccatin12lem1  11502  pfxccatin12lem2  11505  pfxccatin12  11507  swrdccat3blem  11513  shftlem  11583  shftuz  11584  shftfvalg  11585  ovshftex  11586  shftfval  11588  shftval4  11595  shftval5  11596  2shfti  11598  mulreap  11631  sqrt11ap  11806  abs3dif  11873  abs2difabs  11876  maxabslemval  11976  maxle2  11980  maxclpr  11990  2zsupmax  11994  mingeb  12010  2zinfmin  12011  xrmaxiflemval  12018  xrmax2sup  12022  iooinsup  12045  climshftlemg  12070  fsumcnv  12206  explecnv  12274  geo2lim  12285  prodmodc  12347  fprodcnv  12394  demoivre  12542  demoivreALT  12543  nndivides  12566  0dvds  12580  muldvds1  12585  muldvds2  12586  dvdssubr  12608  dvdsadd2b  12609  odd2np1  12642  mulsucdiv2z  12654  ltoddhalfle  12662  ndvdssub  12699  gcdcom  12752  neggcd  12762  gcdabs2  12769  modgcd  12770  bezoutlemaz  12782  dfgcd2  12793  lcmcom  12844  neglcm  12855  lcmgcdeq  12863  coprmdvds  12872  qredeq  12876  divgcdcoprmex  12882  isprm3  12898  prmind2  12900  dvdsprm  12917  cncongrprm  12937  sqrt2irr  12942  hashgcdeq  13020  modprmn0modprm0  13037  coprimeprodsq  13038  pythagtriplem1  13046  pythagtriplem4  13049  pc2dvds  13111  pc11  13112  pcz  13113  pcprod  13127  prmunb  13143  1arithlem2  13145  1arithlem3  13146  1arith  13148  ptex  13620  issubmnd  13757  submcl  13788  resmhm2b  13798  grpinvsub  13889  dfgrp3mlem  13905  imasabl  14142  mgpress  14232  srgmulgass  14295  dfrhm2  14463  isrim0  14470  rmodislmodlem  14689  rmodislmod  14690  cnfldexp  14916  dvdsrzring  14940  znf1o  14988  eltg  15155  eltg2  15156  tgss  15166  tgss2  15182  basgen2  15184  bastop1  15186  opnneiss  15261  cnrest  15338  txss12  15369  hmeofvalg  15406  txswaphmeolem  15423  txswaphmeo  15424  blpnfctr  15542  metequiv  15598  metcnp3  15614  qtopbasss  15624  reopnap  15649  bl2ioo  15653  ioo2bl  15654  ioo2blex  15655  cncfval  15675  divccncfap  15693  addccncf  15703  expcncf  15712  dvexp  15814  dvmptfsum  15828  dvef  15830  efle  15879  reapef  15881  ptolemy  15928  logleb  15980  logdivle  16000  lgsprme0  16173  gausslemma2dlem1a  16189  gausslemma2dlem4  16195  lgsquadlem3  16210  2lgsoddprmlem2  16237  upgrpredgv  16399  uhgr2edg  16459  issubgr  16510  subgrprop  16512  subuhgr  16525  subupgr  16526  subumgr  16527  subusgr  16528  upgriswlkdc  16613  upgrwlkvtxedg  16617  g0wlk0  16623  clwwlkn1  16671  clwwlknonex2lem2  16691  dichmul0orlem3  16767  uzdcinzz  16838  exmidsbthrlem  17079  triap  17090