Theorem ancoms 468

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 450	. 2 ⊢ (𝜓 → (𝜑 → 𝜒))
3	2	imp 444	1 ⊢ ((𝜓 ∧ 𝜑) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 383

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 196  df-an 385

This theorem is referenced by:  adantl  481  syl2anr  494  anim12ci  589  sylan9bbr  733  anabss4  852  anabsi7  856  anabsi8  857  im2anan9r  877  bi2anan9r  914  syl3anr2  1371  mp3anr1  1413  mp3anr2  1414  mp3anr3  1415  stoic1b  1689  19.29rOLD  1791  dvelimf  2322  2eu3  2543  eqeqan12rd  2628  sylan9eqr  2666  r19.29vva  3062  morex  3357  sbcrext  3478  sbcrextOLD  3479  sylan9ssr  3582  pssdifcom1  4006  pssdifcom2  4007  n0snor2el  4304  riinn0  4531  breqan12rd  4600  propeqop  4895  soinxp  5106  frinxp  5107  seinxp  5108  brelrng  5276  dminss  5466  imainss  5467  sossfld  5499  setlikespec  5618  ordelssne  5667  ordtri3or  5672  ordtri2  5675  ordtri4  5678  ordtr3OLD  5687  ordtri2or  5739  funsng  5851  f1co  6023  f1ocnv  6062  f1oprswap  6092  funimass4  6157  dffv2  6181  fndmdifcom  6230  fsn2  6309  fvtp2  6366  fvtp3  6367  fvtp2g  6369  fvtp3g  6370  soisoi  6478  oveqan12rd  6569  brrpssg  6837  sorpsscmpl  6846  dfwe2  6873  ordsucelsuc  6914  ordunisuc2  6936  tfindsg  6952  tfindsg2  6953  dfom2  6959  funcnvuni  7012  fun11iun  7019  cofunex2g  7024  curry2  7159  soxp  7177  mpt2xopoveqd  7234  tposoprab  7275  wfr3g  7300  wfrlem5  7306  wfrlem10  7311  smores3  7337  smores2  7338  smoel  7344  dfrecs3  7356  tfr3  7382  tz7.48-2  7424  tz7.49  7427  oaordi  7513  oaword  7516  oaord1  7518  oaword2  7520  oa00  7526  oalimcl  7527  oaass  7528  oarec  7529  oacomf1o  7532  omord2  7534  omcan  7536  omword  7537  omword1  7540  omword2  7541  odi  7546  omass  7547  oneo  7548  oen0  7553  oecan  7556  oelim2  7562  nnarcl  7583  nnaordi  7585  nnaordr  7587  nnawordi  7588  nnmsucr  7592  nnmcom  7593  nnaword  7594  nnmordi  7598  nnaordex  7605  oaabslem  7610  omabslem  7613  nnneo  7618  omsmo  7621  ersym  7641  elecg  7672  riiner  7707  ecopovsym  7736  ecovcom  7741  mapvalg  7754  pmvalg  7755  elpmg  7759  elmapssres  7768  pmss12g  7770  ixpconstg  7803  ener  7888  enerOLD  7889  domtr  7895  f1imaeng  7902  fundmen  7916  xpcomco  7935  xpsnen2g  7938  xpdom2  7940  xpdom1g  7942  omxpen  7947  omf1o  7948  enen2  7986  domen2  7988  sdomen2  7990  domtriord  7991  sdomel  7992  onsdominel  7994  infensuc  8023  onomeneq  8035  nndomo  8039  pssnn  8063  unbnn  8101  infcntss  8119  fiint  8122  mapfi  8145  fiin  8211  fiss  8213  infempty  8295  oiiso  8325  unwdomg  8372  suc11reg  8399  inf3lem5  8412  infeq5  8417  cantnfp1lem3  8460  r1tr  8522  r1val1  8532  rankr1ai  8544  rankonidlem  8574  onssr1  8577  tskwe  8659  carddom2  8686  carden2  8696  domtri2  8698  cardval2  8700  fidomtri  8702  fidomtri2  8703  harval2  8706  dif1card  8716  infxpenlem  8719  ac5num  8742  alephord3  8784  alephdom  8787  aleph11  8790  alephdom2  8793  cardaleph  8795  dfac3  8827  dfac5  8834  cdacomen  8886  onacda  8902  pwsdompw  8909  ackbij1lem11  8935  ackbij2  8948  cfeq0  8961  cfsuc  8962  cff1  8963  cflim2  8968  cfsmolem  8975  coftr  8978  sornom  8982  infpssrlem4  9011  ssfin4  9015  ssfin2  9025  ssfin3ds  9035  fin23lem31  9048  isf32lem9  9066  hsmexlem5  9135  axdc3lem  9155  axdc3lem2  9156  axdc3lem4  9158  zorn2lem6  9206  brdom3  9231  brdom7disj  9234  brdom6disj  9235  alephval2  9273  alephreg  9283  wuncss  9446  gruen  9513  addcompi  9595  mulcompi  9597  ltapi  9604  ltmpi  9605  nqereu  9630  addcompq  9651  addcomnq  9652  mulcompq  9653  mulcomnq  9654  ltsonq  9670  ltanq  9672  ltmnq  9673  genpnnp  9706  addcompr  9722  mulcompr  9724  ltsopr  9733  ltexprlem2  9738  prlem936  9748  suplem2pr  9754  map2psrpr  9810  axpre-ltadd  9867  xrltnle  9984  axlttri  9988  axsup  9992  ltnle  9996  letri3  10002  leloe  10003  eqlelt  10004  letric  10016  mul31  10083  subcl  10159  pncan2  10167  pncan3  10168  npcan  10169  addsubeq4  10175  npncan3  10198  negsubdi2  10219  muladd  10341  subdi  10342  mulneg2  10346  mulsub  10352  ltleadd  10390  ltsubpos  10399  posdif  10400  addge01  10417  lesub0  10424  wloglei  10439  prodgt02  10748  prodge02  10750  mulsuble0b  10774  ltdivmul  10777  ledivmul  10778  lt2mul2div  10780  lerec  10785  lt2msq  10787  ltdiv23  10793  lediv23  10794  lediv2a  10796  le2msq  10802  msq11  10803  fimaxre  10847  lbreu  10852  infm3  10861  dfinfre  10881  creur  10891  creui  10892  cju  10893  nnmulcl  10920  nndivtr  10939  avgle1  11149  avgle2  11150  avgle  11151  nn0nnaddcl  11201  ltsubnn0  11221  zrevaddcl  11299  znnsub  11300  znn0sub  11301  zextlt  11327  gtndiv  11330  prime  11334  uztrn2  11581  uztric  11585  uz11  11586  nn0pzuz  11621  uzwo  11627  zmax  11661  zbtwnre  11662  rebtwnz  11663  qrevaddcl  11686  rpnnen1lem2  11690  rpnnen1lem1  11691  rpnnen1lem3  11692  rpnnen1lem5  11694  rpnnen1lem1OLD  11697  rpnnen1lem3OLD  11698  rpnnen1lem5OLD  11700  difrp  11744  xrltnsym  11846  xrlttri  11848  xrleloe  11853  xrletri  11860  xrletri3  11861  xrmaxeq  11884  xrmineq  11885  xrmaxlt  11886  xrmaxle  11888  lemaxle  11900  z2ge  11903  qbtwnre  11904  qextlt  11908  qextle  11909  xleneg  11923  xaddcom  11945  xmulcom  11968  xmulneg2  11972  xmulgt0  11985  xrsupsslem  12009  xrinfmsslem  12010  supxrunb1  12021  supxrunb2  12022  ixxssixx  12060  ixxin  12063  ioon0  12072  iccid  12091  iooshf  12123  iccsupr  12137  iooneg  12163  iccneg  12164  iccsplit  12176  fzen  12229  fzadd2  12247  fzass4  12250  fzrev  12273  fznn  12278  elfzp1b  12286  elfzm1b  12287  fz0fzdiffz0  12317  difelfznle  12322  fzon  12358  fzo0n  12359  fzonmapblen  12381  elfzoext  12392  eluzgtdifelfzo  12397  ubmelm1fzo  12430  elfzom1elp1fzo1  12434  subfzo0  12452  fllt  12469  flflp1  12470  flbi  12479  flbi2  12480  flzadd  12489  ltdifltdiv  12497  dfceil2  12502  modcyc2  12568  modifeq2int  12594  modaddmodup  12595  modaddmodlo  12596  modfzo0difsn  12604  modsumfzodifsn  12605  om2uzlt2i  12612  om2uzf1oi  12614  fseqsupubi  12639  fsuppmapnn0fiub0  12655  expcllem  12733  mulbinom2  12846  faclbnd5  12947  hashbnd  12985  hasheni  12998  hasheqf1oi  13002  hasheqf1oiOLD  13003  hashdom  13029  hashss  13058  hashfacen  13095  ccatsymb  13219  ccatass  13224  ccatalpha  13228  wrd2ind  13329  swrdccatin12lem2b  13337  swrdccatin2  13338  swrdccatin12lem2  13340  swrdccatin12  13342  swrdccat3blem  13346  swrdccatid  13348  repswsymball  13377  repswsymballbi  13378  cshwsublen  13393  cshwn  13394  cshwlen  13396  cshwidxmod  13400  cshf1  13407  repswcshw  13409  cshweqdif2  13416  cshweqrep  13418  cshwcsh2id  13425  ccatco  13432  swrdco  13434  lswco  13435  s3iunsndisj  13555  relexprelg  13626  relexpnndm  13629  relexpaddnn  13639  shftlem  13656  shftuz  13657  shftfval  13658  shftval4  13665  shftval5  13666  2shfti  13668  seqshft  13673  mulre  13709  sqrtlt  13850  abs3dif  13919  abs2difabs  13922  uzin2  13932  rexanre  13934  caubnd  13946  climshftlem  14153  rlimcn2  14169  fsumcnv  14346  modfsummods  14366  geo2lim  14445  ntrivcvgfvn0  14470  prodmo  14505  zprod  14506  prodss  14516  fprodcnv  14552  bpolysum  14623  bpoly4  14629  efle  14687  reef11  14688  demoivre  14769  demoivreALT  14770  znnenlem  14779  sqrt2irr  14817  nndivides  14828  0dvds  14840  muldvds1  14844  muldvds2  14845  dvdscmulr  14848  dvdssubr  14865  dvdsadd2b  14866  odd2np1  14903  mulsucdiv2z  14915  ltoddhalfle  14923  divalglem9  14962  ndvdssub  14971  gcdcllem1  15059  gcdcom  15073  neggcd  15082  gcdabs2  15090  modgcd  15091  lcmcom  15144  neglcm  15155  lcmgcdeq  15163  coprmdvds  15204  coprmdvdsOLD  15205  qredeq  15209  divgcdcoprmex  15218  dvdsprm  15253  cncongrprm  15275  odzdvds  15338  powm2modprm  15346  modprmn0modprm0  15350  coprimeprodsq  15351  pythagtriplem1  15359  pythagtriplem4  15362  pc2dvds  15421  pc11  15422  pcz  15423  pcprod  15437  prmunb  15456  1arithlem3  15467  1arith  15469  cshwshashlem2  15641  cshwshashlem3  15642  ressabs  15766  acsfn2  16147  issect  16236  funcestrcsetclem9  16611  funcsetcestrclem5  16622  funcsetcestrclem9  16626  pospo  16796  latjcom  16882  latmcom  16898  clatglbss  16950  pospropd  16957  pslem  17029  tsrss  17046  issubmnd  17141  submcl  17176  resmhm2b  17184  frmdmnd  17219  frmd0  17220  grpinvsub  17320  dfgrp3lem  17336  gimcnv  17532  gimco  17533  gictr  17540  cntz2ss  17588  cntzrec  17589  symg2bas  17641  symgextf1  17664  symgfixelsi  17678  pmtrfinv  17704  pmtrdifwrdel2  17729  dfod2  17804  lsmcom2  17893  efgred  17984  qusabl  18091  cygabl  18115  gsummptnn0fz  18205  eldprd  18226  srgmulgass  18354  dfrhm2  18540  isrim0  18546  lmimcnv  18888  mplcoe5lem  19288  psrbagfsupp  19330  cnfldexp  19598  cnsrng  19599  xrsdsreval  19610  dvdsrzring  19650  znf1o  19719  ocvocv  19834  ocvin  19837  frlmip  19936  islindf  19970  lindff  19973  lindfrn  19979  f1lindf  19980  mamudir  20029  matsca2  20045  matbas2  20046  matlmod  20054  matinvgcell  20060  mat1bas  20074  dmatmul  20122  dmatsgrp  20124  dmatsrng  20126  dmatcrng  20127  scmatsgrp1  20147  scmatsrng1  20148  madulid  20270  gsummatr01lem3  20282  gsummatr01  20284  cpmatacl  20340  0mat2pmat  20360  idmatidpmat  20361  m2cpminv0  20385  pmatcollpw3fi1lem1  20410  chfacfscmulgsum  20484  chfacfpmmulgsum  20488  eltg  20572  eltg2  20573  tgss  20583  tgss2  20602  basgen2  20604  bastop1  20608  cldmre  20692  toponmre  20707  opnneiss  20732  restcldr  20788  restfpw  20793  restcls  20795  restntr  20796  ordtbaslem  20802  ordtrest2lem  20817  leordtvallem2  20825  leordtval  20827  cnrest  20899  t0sep  20938  cmpcov  21002  cmpsublem  21012  cmpsub  21013  bwth  21023  2ndcomap  21071  locfincmp  21139  ptval  21183  xkoval  21200  txss12  21218  ptrescn  21252  xkopt  21268  hmeofval  21371  txswaphmeolem  21417  txswaphmeo  21418  trfbas2  21457  trfbas  21458  uzrest  21511  numufl  21529  ssufl  21532  flimclsi  21592  hauspwpwf1  21601  ghmcnp  21728  blpnfctr  22051  metequiv  22124  metcnp3  22155  elbl4  22178  restmetu  22185  tngngp  22268  qtopbaslem  22372  bl2ioo  22403  ioo2bl  22404  ioo2blex  22405  xrsxmet  22420  divccn  22484  divccncf  22517  isclmi0  22706  iscvsi  22737  causs  22904  lmclim  22909  bcthlem1  22929  ovolfsf  23047  ioombl  23140  iccvolcl  23142  ioovolcl  23144  ioorcl  23151  volcn  23180  itg2itg1  23309  dvexp  23522  dvmptfsum  23542  dvexp3  23545  dvef  23547  dvlip  23560  c1lip1  23564  ftc1a  23604  tdeglem1  23622  tdeglem3  23623  tdeglem4  23624  coe1termlem  23818  plyremlem  23863  ptolemy  24052  cos11  24083  logeftb  24134  logleb  24153  logdivlt  24171  logdivle  24172  angval  24331  isppw2  24641  issqf  24662  vmasum  24741  lgsprme0  24864  gausslemma2dlem1a  24890  lgsquadlem3  24907  2lgsoddprmlem2  24934  ostth  25128  brbtwn2  25585  colinearalglem4  25589  ax5seglem1  25608  ax5seglem2  25609  axcontlem2  25645  axcontlem12  25655  nb3graprlem2  25981  isspthonpth  26114  wlkdvspthlem  26137  3v3e3cycl1  26172  constr3trllem2  26179  constr3trllem3  26180  wwlknimp  26215  wlkiswwlk2  26225  wwlknextbi  26253  wwlknfi  26266  wwlkextprop  26272  clwwlkfo  26325  clwwnisshclwwn  26337  erclwwlksym  26342  erclwwlktr  26343  erclwwlknsym  26354  erclwwlkntr  26355  eupatrl  26495  frgra3v  26529  frgraregorufr  26580  usg2spot2nb  26592  numclwwlkun  26606  numclwwlk1  26625  frgraregord013  26645  vcz  26814  isvcOLD  26818  isnv  26851  isnvi  26852  nmooge0  27006  nmblolbii  27038  blocnilem  27043  ipblnfi  27095  hvpncan2  27281  hvaddsub4  27319  hire  27335  abshicom  27342  hial2eq2  27348  orthcom  27349  hhssabloi  27503  ocsh  27526  shscli  27560  shscom  27562  shsel2  27565  spanss  27591  shjcom  27601  shmodsi  27632  chpsscon3  27746  spansni  27800  spansnmul  27807  spansncol  27811  spanunsni  27822  cmcm2  27859  cm2j  27863  spansncvi  27895  5oalem2  27898  3oalem2  27906  honegsubdi2  28054  adjsym  28076  cnvadj  28135  brafn  28190  kbpj  28199  riesz3i  28305  cnlnadjlem2  28311  cnlnadjlem9  28318  nmopcoi  28338  cnvbraval  28353  leop  28366  leop3  28368  leopmul2i  28378  leoptri  28379  hstrlem3a  28503  cvcon3  28527  cvnsym  28533  mdbr2  28539  dmdmd  28543  dmdbr2  28546  dmdbr3  28548  dmdbr4  28549  dmdbr5  28551  mdsl0  28553  ssmd2  28555  mdslmd1lem1  28568  mdslmd1lem2  28569  mdslmd3i  28575  mdslmd4i  28576  atcveq0  28591  superpos  28597  atnemeq0  28620  atssma  28621  atexch  28624  atomli  28625  atcvatlem  28628  atcvati  28629  chirredlem1  28633  chirredlem3  28635  chirredi  28637  atcvat3i  28639  atdmd  28641  mdsymlem1  28646  mdsymlem3  28648  mdsymlem4  28649  mdsymlem5  28650  mdsymlem8  28653  dmdsym  28656  atdmd2  28657  sumdmdlem  28661  cdjreui  28675  cdj3lem2b  28680  cdj3i  28684  imadifxp  28796  abfmpel  28835  xaddeq0  28907  xrofsup  28923  xeqlelt  28928  xdivpnfrp  28972  xrsinvgval  29008  xrsmulgzz  29009  pcmplfin  29255  cnvordtrestixx  29287  ordtrest2NEWlem  29296  indval  29403  esumpfinvallem  29463  sigagenss  29539  ddemeas  29626  brae  29631  dya2iocival  29662  dya2iocnei  29671  dya2iocuni  29672  omsf  29685  oddpwdc  29743  bnj934  30259  derangenlem  30407  subfacval2  30423  kur14  30452  lediv2aALT  30825  faclim2  30887  funpsstri  30909  dftrpred3g  30977  soseq  30995  wsuclem  31017  wsuclemOLD  31018  frrlem5  31028  elno  31043  nosepon  31066  sltsolem1  31067  nodenselem4  31083  nofulllem5  31105  hfelhf  31458  elicc3  31481  nn0prpwlem  31487  nn0prpw  31488  isfne  31504  onsuct0  31610  nndivsub  31626  bj-ssbequ2  31832  bj-restsnss  32217  bj-restsnss2  32218  bj-restuni2  32232  topdifinffinlem  32371  iooelexlt  32386  relowlssretop  32387  rdgeqoa  32394  wl-sbcom2d-lem1  32521  wl-sbcom2d  32523  wl-ax11-lem6  32546  curf  32557  finixpnum  32564  ltflcei  32567  leceifl  32568  cos2h  32570  matunitlindflem1  32575  matunitlindflem2  32576  matunitlindf  32577  ptrecube  32579  poimirlem6  32585  poimirlem7  32586  poimirlem10  32589  poimirlem11  32590  poimirlem27  32606  poimirlem29  32608  poimirlem30  32609  poimirlem31  32610  poimirlem32  32611  mblfinlem3  32618  mblfinlem4  32619  ismblfin  32620  ovoliunnfl  32621  voliunnfl  32623  volsupnfl  32624  cnambfre  32628  itg2addnclem2  32632  itg2addnc  32634  itg2gt0cn  32635  ftc1anclem1  32655  ftc1anclem4  32658  ftc1anclem6  32660  ftc1anclem7  32661  ftc1anc  32663  unirep  32677  opelopab3  32681  fvopabf4g  32685  indexa  32698  filbcmb  32705  incsequz2  32715  metf1o  32721  sstotbnd3  32745  isbnd2  32752  bndss  32755  ismtycnv  32771  iccbnd  32809  exidreslem  32846  exidresid  32848  ghomco  32860  isdivrngo  32919  isdrngo2  32927  rngoisocnv  32950  riscer  32957  crngohomfo  32975  unichnidl  33000  maxidlmax  33012  igenmin  33033  exmid2  33071  orel  33074  prtlem16  33172  paddss1  34121  paddss2  34122  paddss12  34123  pclfinN  34204  erngmul-rN  35120  mapdordlem2  35944  ismrc  36282  nacsfg  36286  isnacs3  36291  incssnn0  36292  mzpclall  36308  lerabdioph  36387  ltrabdioph  36390  eldioph4b  36393  jm2.17b  36546  congrep  36558  lnr2i  36705  rp-fakenanass  36879  brnonrel  36914  enrelmap  37311  enrelmapr  37312  rcompleq  37338  isotone1  37366  isotone2  37367  radcnvrat  37535  expgrowth  37556  bcc0  37561  binomcxplemnn0  37570  2sbc6g  37638  2sbc5g  37639  ordpss  37676  addrcom  37700  3impcombi  38065  sspwimp  38176  sspwimpVD  38177  ax6e2ndeqALT  38189  iunconlem2  38193  sineq0ALT  38195  nsstr  38301  iunmapsn  38404  ssfiunibd  38464  fmul01  38647  lptre2pt  38707  stoweidlem34  38927  dirkeritg  38995  fourierdlem73  39072  sigarac  39690  2reu3  39837  afv0nbfvbi  39880  dmfcoafv  39904  elmod2  39950  fmtnofac2lem  40018  prmdvdsfmtnof1lem2  40035  proththd  40069  opoeALTV  40132  opeoALTV  40133  epoo  40150  evenprm2  40161  gbegt5  40183  sgoldbaltlem2  40202  nnsum4primeseven  40216  nnsum4primesevenALTV  40217  bgoldbtbndlem4  40224  bgoldbtbnd  40225  pfxccatin12lem1  40286  pfxccatin12lem2  40287  pfxccatin12  40288  riotaeqimp  40338  cnambpcma  40341  ltnltne  40345  fzoopth  40360  uhgr2edg  40435  issubgr  40495  subgrprop  40497  subuhgr  40510  subupgr  40511  subumgr  40512  subusgr  40513  nb3grprlem2  40609  cplgr3v  40657  1wlk1walk  40843  upgr1wlkvtxedg  40853  pthdivtx  40935  usgr2trlncl  40966  crctcsh1wlkn0lem3  41015  crctcsh1wlkn0lem6  41018  crctcsh1wlkn0lem7  41019  crctcsh1wlkn0  41024  1wlkiswwlks2  41072  wwlksnextbi  41100  wwlksnfi  41112  wwlksnextprop  41118  clwwlksfo  41225  erclwwlkssym  41242  erclwwlksnsym  41254  is01wlk  41285  is0Trl  41291  3pthdlem1  41331  frgr3v  41445  frgrregorufr  41490  av-numclwwlkovfel2  41514  av-numclwwlk1  41528  av-numclwlk2lem2f  41533  av-numclwlk2lem2f1o  41535  av-frgraregord013  41549  submgmcl  41584  resmgmhm2b  41590  isassintop  41636  rnghmval  41681  isrngisom  41686  c0snghm  41706  zrrnghm  41707  2zrngamgm  41729  rnghmsubcsetclem2  41768  rhmsubcsetclem2  41814  rhmsubcrngclem1  41819  rhmsubcrngclem2  41820  funcringcsetcALTV2lem9  41836  funcringcsetclem9ALTV  41859  rhmsubclem4  41881  rhmsubcALTVlem4  41900  cbvmpt2x2  41907  nn0sumltlt  41921  gsumlsscl  41958  ply1mulgsumlem1  41968  lincvalpr  42001  lincdifsn  42007  linc1  42008  lincellss  42009  islinindfiss  42033  islindeps  42036  lincresunit2  42061  islininds2  42067  lmod1zr  42076  ltsubadd2b  42100  zgtp1leeq  42105  logblt1b  42156  blengt1fldiv2p1  42185  nn0sumshdiglemB  42212  aacllem  42356