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  6530  tposoprab  6556  smores3  6569  smores2  6570  smoel  6576  tfri3  6643  rdgtfr  6650  rdgruledefgg  6651  omcl  6739  oeicl  6740  nnmsucr  6766  nnmcom  6767  nndir  6768  nnaordi  6786  nnaordr  6788  nnaword  6789  nnmordi  6794  nnaordex  6806  nnm00  6808  ersym  6824  elecg  6852  riinerm  6887  ecopovsym  6910  ecopovsymg  6913  ecovcom  6921  ecovicom  6922  mapvalg  6937  pmvalg  6938  elpmg  6943  elmapssres  6959  pmss12g  6961  ixpconstg  6995  domssr  7070  ener  7072  domtr  7078  f1imaeng  7085  fundmen  7100  xpcomco  7130  xpsnen2g  7133  xpdom2  7135  xpdom1g  7137  enen2  7147  domen2  7149  ssfilem  7183  ssfilemd  7185  diffitest  7197  fiintim  7244  fundmfibi  7258  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  9698  zrevaddcl  9705  znnsub  9706  znn0sub  9720  ltsubnn0  9722  zdclt  9732  zextlt  9749  gtndiv  9752  prime  9756  peano5uzti  9765  uztrn2  9956  uztric  9960  uz11  9961  nn0pzuz  10003  indstr  10009  supinfneg  10011  infsupneg  10012  eluzdc  10026  qrevaddcl  10060  difrp  10110  xrltnsym  10212  xrltso  10215  xrlttri3  10216  xrletri3  10223  xleneg  10256  xaddcom  10280  xposdif  10301  ixxssixx  10321  iccid  10344  iooshf  10371  iccsupr  10385  iooneg  10407  iccneg  10408  fztri3or  10460  fzdcel  10461  fzn  10463  fzen  10464  fzass4  10485  fzrev  10508  fznn  10513  elfzp1b  10521  elfzm1b  10522  fz0fzdiffz0  10554  difelfznle  10559  fzon  10591  fzo0n  10592  fzonmapblen  10616  elfzoextl  10626  eluzgtdifelfzo  10632  ubmelm1fzo  10661  subfzo0  10678  qletric  10693  qdclt  10697  qdcle  10698  ioo0  10711  ico0  10713  ioc0  10714  flqbi  10746  flqbi2  10747  flqzadd  10754  modfzo0difsn  10853  fzfig  10888  expcllem  11008  expap0  11027  mulbinom2  11114  expnbnd  11122  sq11ap  11166  hashfacen  11306  iswrdinn0  11331  ccatsymb  11392  ccatalpha  11403  swrd0g  11454  swrdsbslen  11460  swrdspsleq  11461  wrd2ind  11517  pfxccatin12lem1  11522  pfxccatin12lem2  11525  pfxccatin12  11527  swrdccat3blem  11533  shftlem  11603  shftuz  11604  shftfvalg  11605  ovshftex  11606  shftfval  11608  shftval4  11615  shftval5  11616  2shfti  11618  mulreap  11651  sqrt11ap  11826  abs3dif  11894  abs2difabs  11897  maxabslemval  11997  maxle2  12001  maxclpr  12011  2zsupmax  12015  mingeb  12033  2zinfmin  12034  xrmaxiflemval  12041  xrmax2sup  12045  iooinsup  12068  climshftlemg  12093  fsumcnv  12229  explecnv  12297  geo2lim  12308  prodmodc  12370  fprodcnv  12417  demoivre  12565  demoivreALT  12566  nndivides  12589  0dvds  12603  muldvds1  12608  muldvds2  12609  dvdssubr  12631  dvdsadd2b  12632  odd2np1  12665  mulsucdiv2z  12677  ltoddhalfle  12685  ndvdssub  12722  gcdcom  12775  neggcd  12785  gcdabs2  12792  modgcd  12793  bezoutlemaz  12805  dfgcd2  12816  lcmcom  12867  neglcm  12878  lcmgcdeq  12886  coprmdvds  12895  qredeq  12899  divgcdcoprmex  12905  isprm3  12921  prmind2  12923  dvdsprm  12941  cncongrprm  12961  sqrt2irr  12966  nnmaxpw  12978  hashgcdeq  13047  modprmn0modprm0  13064  coprimeprodsq  13065  pythagtriplem1  13073  pythagtriplem4  13076  pc2dvds  13138  pc11  13139  pcz  13140  pcprod  13154  prmunb  13170  1arithlem2  13172  1arithlem3  13173  1arith  13175  ptex  13677  issubmnd  13814  submcl  13845  resmhm2b  13855  grpinvsub  13946  dfgrp3mlem  13962  cntz2ss  14168  cntzrec  14169  imasabl  14230  mgpress  14337  srgmulgass  14400  dfrhm2  14570  isrim0  14577  rmodislmodlem  14796  rmodislmod  14797  cnfldexp  15023  dvdsrzring  15047  znf1o  15095  eltg  15311  eltg2  15312  tgss  15322  tgss2  15338  basgen2  15340  bastop1  15342  opnneiss  15417  cnrest  15494  txss12  15525  hmeofvalg  15562  txswaphmeolem  15579  txswaphmeo  15580  blpnfctr  15698  metequiv  15754  metcnp3  15770  qtopbasss  15780  reopnap  15805  bl2ioo  15809  ioo2bl  15810  ioo2blex  15811  cncfval  15831  divccncfap  15849  addccncf  15859  expcncf  15868  dvexp  15970  dvmptfsum  15984  dvef  15986  efle  16035  reapef  16037  ptolemy  16084  logleb  16138  logdivle  16158  lgsprme0  16399  gausslemma2dlem1a  16415  gausslemma2dlem4  16421  lgsquadlem3  16436  2lgsoddprmlem2  16463  upgrpredgv  16625  uhgr2edg  16685  issubgr  16736  subgrprop  16738  subuhgr  16751  subupgr  16752  subumgr  16753  subusgr  16754  upgriswlkdc  16839  upgrwlkvtxedg  16843  g0wlk0  16849  clwwlkn1  16897  clwwlknonex2lem2  16917  dichmul0orlem3  16993  uzdcinzz  17064  exmidsbthrlem  17306  triap  17317