Theorem ancoms 459

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  pm3.22  460  adantl  482  sylan9bbr  511  syl2anr  596  anim12ci  613  im2anan9r  620  bi2anan9r  636  anabss4  663  anabsi7  667  anabsi8  668  mp3anr1  1450  mp3anr2  1451  mp3anr3  1452  stoic1b  1756  dvelimf  2426  2eu3  2708  2eu3OLD  2709  eqeqan12rd  2812  sylan9eqr  2852  r19.29r  3218  r19.29vvaOLD  3297  cbvrexdva2  3407  morex  3647  sbcrext  3786  sylan9ssr  3905  pssdifcom1  4351  pssdifcom2  4352  preq12nebg  4702  opthprneg  4704  riinn0  4906  breqan12rd  4981  snopeqop  5290  propeqop  5291  soinxp  5522  frinxp  5523  seinxp  5524  brelrng  5696  dminss  5889  imainss  5890  sossfld  5922  cnvsng  5958  setlikespec  6047  ordelssne  6096  ordtri3or  6101  ordtri2  6104  ordtri4  6106  ordtri2or  6164  funsng  6278  f1co  6456  f1oprswap  6529  funimass4  6601  dffv2  6626  fndmdifcom  6681  fsn2  6764  fvtp2  6828  fvtp3  6829  fvtp2g  6831  fvtp3g  6832  soisoi  6947  riotaeqimp  7003  oveqan12rd  7039  brrpssg  7312  sorpsscmpl  7321  dfwe2  7355  ordsucelsuc  7396  ordunisuc2  7418  tfindsg  7434  tfindsg2  7435  dfom2  7441  funcnvuni  7495  fiunlem  7502  cofunex2g  7510  curry2  7661  soxp  7679  mpoxopoveqd  7741  tposoprab  7782  wfr3g  7807  wfrlem5  7814  wfrlem10  7819  smores3  7845  smores2  7846  smoel  7852  tfr3  7890  tz7.48-2  7932  tz7.49  7935  oaordi  8025  oaword  8028  oaord1  8030  oaword2  8032  oa00  8038  oalimcl  8039  oaass  8040  oarec  8041  oacomf1o  8044  omord2  8046  omcan  8048  omword  8049  omword1  8052  omword2  8053  odi  8058  omass  8059  oneo  8060  oen0  8065  oecan  8068  oelim2  8074  nnarcl  8095  nnaordi  8097  nnaordr  8099  nnawordi  8100  nnmsucr  8104  nnmcom  8105  nnaword  8106  nnmordi  8110  nnaordex  8117  oaabslem  8123  omabslem  8126  nnneo  8131  omsmo  8134  ersym  8154  elecg  8185  riiner  8223  ecopovsym  8252  ecovcom  8256  mapvalg  8269  pmvalg  8270  elpmg  8275  elmapssres  8284  pmss12g  8286  ixpconstg  8322  ener  8407  domtr  8413  f1imaeng  8420  fundmen  8434  xpcomco  8457  xpsnen2g  8460  xpdom2  8462  xpdom1g  8464  omxpen  8469  omf1o  8470  enen2  8508  domen2  8510  sdomen2  8512  domtriord  8513  sdomel  8514  onsdominel  8516  infensuc  8545  onomeneq  8557  nndomo  8561  pssnn  8585  unbnn  8623  fiint  8644  mapfi  8669  fiin  8735  fiss  8737  infempty  8820  oiiso  8850  unwdomg  8897  suc11reg  8931  inf3lem5  8944  infeq5  8949  cantnfp1lem3  8992  r1tr  9054  r1val1  9064  rankr1ai  9076  rankonidlem  9106  onssr1  9109  djuex  9186  djuunxp  9199  tskwe  9228  carddom2  9255  carden2  9265  domtri2  9267  cardval2  9269  fidomtri  9271  fidomtri2  9272  harval2  9275  dif1card  9285  infxpenlem  9288  ac5num  9311  alephord3  9353  alephdom  9356  aleph11  9359  alephdom2  9362  cardaleph  9364  dfac3  9396  dfac5  9403  onadju  9468  pwsdompw  9475  ackbij1lem11  9501  ackbij2  9514  cfeq0  9527  cfsuc  9528  cff1  9529  cflim2  9534  cfsmolem  9541  coftr  9544  sornom  9548  infpssrlem4  9577  ssfin4  9581  ssfin2  9591  ssfin3ds  9601  fin23lem31  9614  isf32lem9  9632  hsmexlem5  9701  axdc3lem  9721  axdc3lem2  9722  axdc3lem4  9724  zorn2lem6  9772  brdom3  9799  brdom7disj  9802  brdom6disj  9803  alephval2  9843  alephreg  9853  wuncss  10016  gruen  10083  addcompi  10165  mulcompi  10167  ltapi  10174  ltmpi  10175  nqereu  10200  addcompq  10221  addcomnq  10222  mulcompq  10223  mulcomnq  10224  ltsonq  10240  ltanq  10242  ltmnq  10243  genpnnp  10276  addcompr  10292  mulcompr  10294  ltsopr  10303  ltexprlem2  10308  prlem936  10318  suplem2pr  10324  map2psrpr  10381  axpre-ltadd  10438  xrltnle  10557  axlttri  10561  axsup  10565  ltnle  10569  letri3  10575  leloe  10576  eqlelt  10577  letric  10589  mul31  10656  subcl  10734  pncan2  10742  pncan3  10743  pncan3OLD  10744  npcan  10745  addsubeq4  10751  npncan3  10774  negsubdi2  10795  muladd  10922  subdi  10923  mulneg2  10927  mulsub  10933  ltleadd  10973  ltsubpos  10982  posdif  10983  addge01  11000  lesub0  11007  wloglei  11022  prodgt02  11338  mulsuble0b  11362  ltdivmul  11365  ledivmul  11366  lt2mul2div  11368  lerec  11373  lt2msq  11375  ltdiv23  11381  lediv23  11382  le2msq  11390  msq11  11391  fimaxreOLD  11435  infm3  11450  dfinfre  11472  creur  11482  creui  11483  cju  11484  nnmulcl  11511  nndivtr  11534  avgle1  11727  avgle2  11728  avgle  11729  nn0nnaddcl  11778  ltsubnn0  11798  zrevaddcl  11877  znnsub  11878  znn0sub  11879  zextlt  11906  gtndiv  11909  prime  11913  uztrn2  12111  uztric  12115  uz11  12116  nn0pzuz  12154  uzwo  12160  zmax  12194  zbtwnre  12195  rebtwnz  12196  qrevaddcl  12220  rpnnen1lem2  12226  rpnnen1lem1  12227  rpnnen1lem3  12228  rpnnen1lem5  12230  difrp  12277  xrltnsym  12380  xrlttri  12382  xrleloe  12387  xrletri  12396  xrletri3  12397  xrmaxeq  12422  xrmineq  12423  xrmaxlt  12424  xrmaxle  12426  lemaxle  12438  z2ge  12441  qbtwnre  12442  qextlt  12446  qextle  12447  xleneg  12461  xaddcom  12483  xmulcom  12509  xmulneg2  12513  xmulgt0  12526  xrsupsslem  12550  xrinfmsslem  12551  supxrunb1  12562  supxrunb2  12563  ixxssixx  12602  ixxin  12605  ioon0  12614  iccid  12633  iooshf  12665  iccsupr  12680  iooneg  12707  iccneg  12708  iccsplit  12721  fzen  12774  fzadd2  12792  fzass4  12795  fzrev  12820  fznn  12825  elfzp1b  12834  elfzm1b  12835  fz0fzdiffz0  12866  difelfznle  12871  fzon  12908  fzo0n  12909  fzonmapblen  12933  elfzoext  12944  eluzgtdifelfzo  12949  ubmelm1fzo  12983  elfzom1elp1fzo1  12987  subfzo0  13009  fllt  13026  flflp1  13027  flbi  13036  flbi2  13037  flzadd  13046  ltdifltdiv  13054  modcyc2  13125  modifeq2int  13151  modaddmodup  13152  modaddmodlo  13153  modfzo0difsn  13161  modsumfzodifsn  13162  om2uzlt2i  13169  om2uzf1oi  13171  fseqsupubi  13196  fsuppmapnn0fiub0  13211  expcllem  13290  mulbinom2  13434  expnngt1  13452  faclbnd5  13508  hashbnd  13546  hasheni  13558  hasheqf1oi  13562  hashdom  13588  hashunsnggt  13603  hashss  13618  hashgt23el  13633  hashfacen  13660  ccatsymb  13780  ccatass  13786  ccatalpha  13791  wrd2ind  13921  pfxccatin12lem1  13926  swrdccatin2  13927  pfxccatin12lem2  13929  pfxccatin12  13931  swrdccat3blem  13937  repswsymballbi  13978  cshwsublen  13994  cshwn  13995  cshwlen  13997  cshwidxmod  14001  cshf1  14008  repswcshw  14010  cshweqdif2  14017  cshweqrep  14019  cshwcsh2id  14026  ccatco  14033  swrdco  14035  lswco  14037  s3iunsndisj  14162  relexprelg  14231  relexpnndm  14234  relexpaddnn  14244  shftlem  14261  shftuz  14262  shftfval  14263  shftval4  14270  shftval5  14271  2shfti  14273  seqshft  14278  mulre  14314  sqrtlt  14455  abs3dif  14525  abs2difabs  14528  uzin2  14538  rexanre  14540  caubnd  14552  climshftlem  14765  rlimcn2  14781  fsumcnv  14961  modfsummods  14981  geo2lim  15064  ntrivcvgfvn0  15088  prodmo  15123  zprod  15124  prodss  15134  fprodcnv  15170  bpolysum  15240  bpoly4  15246  efle  15304  reef11  15305  demoivre  15386  demoivreALT  15387  sqrt2irr  15435  nndivides  15450  0dvds  15463  muldvds1  15467  muldvds2  15468  dvdscmulr  15471  dvdssubr  15488  dvdsadd2b  15489  odd2np1  15523  mulsucdiv2z  15535  ltoddhalfle  15543  divalglem9  15585  gcdcllem1  15681  gcdcom  15695  neggcd  15704  gcdabs2  15712  modgcd  15713  lcmcom  15766  neglcm  15777  lcmgcdeq  15785  coprmdvds  15826  qredeq  15830  divgcdcoprmex  15839  cncongrprm  15898  odzdvds  15961  modprmn0modprm0  15973  coprimeprodsq  15974  pythagtriplem1  15982  pythagtriplem4  15985  pc2dvds  16044  pc11  16045  pcz  16046  pcprod  16060  prmunb  16079  1arithlem3  16090  1arith  16092  cshwshashlem3  16260  ressabs  16392  acsfn2  16763  issect  16852  funcestrcsetclem9  17227  funcsetcestrclem5  17238  funcsetcestrclem9  17242  pospo  17412  latjcom  17498  latmcom  17514  clatglbss  17566  pospropd  17573  pslem  17645  tsrss  17662  issubmnd  17757  submcl  17792  resmhm2b  17800  frmdmnd  17835  frmd0  17836  grpinvsub  17938  dfgrp3lem  17954  gimco  18149  gictr  18156  cntz2ss  18204  cntzrec  18205  symg2bas  18257  symgextf1  18280  symgfixelsi  18294  pmtrfinv  18320  pmtrdifwrdel2  18345  dfod2  18421  lsmcom2  18510  efgred  18601  qusabl  18708  cygabl  18732  eldprd  18843  srgmulgass  18971  dfrhm2  19159  isrim0  19165  rmodislmodlem  19391  rmodislmod  19392  mplcoe5lem  19935  psrbagfsupp  19976  cnfldexp  20260  cnsrng  20261  xrsdsreval  20272  dvdsrzring  20312  znf1o  20380  ocvocv  20497  ocvin  20500  frlmip  20604  islindf  20638  lindff  20641  lindfrn  20647  f1lindf  20648  mamudir  20697  matsca2  20713  matlmod  20722  matinvgcell  20728  mat1bas  20742  dmatmul  20790  dmatsgrp  20792  dmatsrng  20794  dmatcrng  20795  scmatsgrp1  20815  scmatsrng1  20816  madulid  20938  gsummatr01lem3  20950  gsummatr01  20952  cpmatacl  21008  0mat2pmat  21028  idmatidpmat  21029  m2cpminv0  21053  pmatcollpw3fi1lem1  21078  chfacfscmulgsum  21152  chfacfpmmulgsum  21156  eltg  21249  eltg2  21250  tgss  21260  tgss2  21279  basgen2  21281  bastop1  21285  cldmre  21370  toponmre  21385  opnneiss  21410  restcldr  21466  restfpw  21471  restcls  21473  restntr  21474  ordtbaslem  21480  ordtrest2lem  21495  leordtvallem2  21503  leordtval  21505  cnrest  21577  t0sep  21616  cmpcov  21681  cmpsublem  21691  cmpsub  21692  bwth  21702  2ndcomap  21750  locfincmp  21818  ptval  21862  xkoval  21879  txss12  21897  ptrescn  21931  xkopt  21947  hmeofval  22050  txswaphmeolem  22096  txswaphmeo  22097  trfbas2  22135  trfbas  22136  uzrest  22189  numufl  22207  ssufl  22210  flimclsi  22270  hauspwpwf1  22279  ghmcnp  22406  blpnfctr  22729  metequiv  22802  metcnp3  22833  elbl4  22856  restmetu  22863  tngngp  22946  qtopbaslem  23050  bl2ioo  23083  ioo2bl  23084  ioo2blex  23085  xrsxmet  23100  divccn  23164  divccncf  23197  isclmi0  23385  iscvsi  23416  causs  23584  lmclim  23589  bcthlem1  23610  ovolfsf  23755  ioombl  23849  iccvolcl  23851  ioovolcl  23854  ioorcl  23861  volcn  23890  itg2itg1  24020  dvexp  24233  dvmptfsum  24255  dvexp3  24258  dvef  24260  dvlip  24273  c1lip1  24277  ftc1a  24317  tdeglem1  24335  tdeglem3  24336  tdeglem4  24337  coe1termlem  24531  plyremlem  24576  ptolemy  24765  cos11  24798  logeftb  24848  logleb  24867  logdivlt  24885  logdivle  24886  angval  25060  isppw2  25374  issqf  25395  vmasum  25474  lgsprme0  25597  gausslemma2dlem1a  25623  lgsquadlem3  25640  2lgsoddprmlem2  25667  ostth  25897  brbtwn2  26374  colinearalglem4  26378  ax5seglem1  26397  ax5seglem2  26398  axcontlem2  26434  axcontlem12  26444  upgrpredgv  26607  uhgr2edg  26673  issubgr  26736  subgrprop  26738  subuhgr  26751  subupgr  26752  subumgr  26753  subusgr  26754  nb3grprlem2  26846  cplgr3v  26900  wlk1walk  27103  upgrwlkvtxedg  27109  pthdivtx  27192  crctcshwlkn0lem3  27272  crctcshwlkn0lem6  27275  crctcshwlkn0lem7  27276  crctcshwlkn0  27281  wlkiswwlks2  27335  wwlksnfiOLD  27367  wwlksnextprop  27373  erclwwlksym  27481  clwwlkn1  27501  clwwlkfo  27511  erclwwlknsym  27531  clwwlknonex2lem2  27569  is0wlk  27578  is0trl  27584  3pthdlem1  27625  frgr3v  27738  frgrncvvdeqlem3  27764  frgrregorufr  27788  clwwnonrepclwwnon  27808  extwwlkfab  27815  numclwwlk1  27824  numclwlk2lem2f  27840  numclwlk2lem2f1o  27842  vcz  28035  isvcOLD  28039  isnv  28072  isnvi  28073  nmooge0  28227  nmblolbii  28259  blocnilem  28264  ipblnfi  28315  hvpncan2  28500  hvaddsub4  28538  hire  28554  abshicom  28561  hial2eq2  28567  orthcom  28568  hhssabloi  28722  ocsh  28743  shscli  28777  shscom  28779  shsel2  28782  spanss  28808  shjcom  28818  shmodsi  28849  chpsscon3  28963  spansni  29017  spansnmul  29024  spansncol  29028  spanunsni  29039  cmcm2  29076  cm2j  29080  spansncvi  29112  5oalem2  29115  3oalem2  29123  honegsubdi2  29271  adjsym  29293  cnvadj  29352  brafn  29407  kbpj  29416  riesz3i  29522  cnlnadjlem2  29528  cnlnadjlem9  29535  nmopcoi  29555  cnvbraval  29570  leop  29583  leop3  29585  leopmul2i  29595  leoptri  29596  hstrlem3a  29720  cvcon3  29744  cvnsym  29750  mdbr2  29756  dmdmd  29760  dmdbr2  29763  dmdbr3  29765  dmdbr4  29766  dmdbr5  29768  mdsl0  29770  ssmd2  29772  mdslmd1lem1  29785  mdslmd1lem2  29786  mdslmd3i  29792  mdslmd4i  29793  atcveq0  29808  superpos  29814  atnemeq0  29837  atssma  29838  atexch  29841  atomli  29842  atcvatlem  29845  atcvati  29846  chirredlem1  29850  chirredlem3  29852  chirredi  29854  atcvat3i  29856  atdmd  29858  mdsymlem1  29863  mdsymlem3  29865  mdsymlem4  29866  mdsymlem5  29867  mdsymlem8  29870  dmdsym  29873  atdmd2  29874  sumdmdlem  29878  cdjreui  29892  cdj3lem2b  29897  cdj3i  29901  r19.29ffa  29921  opreu2reuALT  29924  imadifxp  30033  abfmpel  30082  xaddeq0  30157  xrofsup  30172  xnn0gt0  30174  xeqlelt  30179  xdivpnfrp  30285  xrsinvgval  30330  xrsmulgzz  30331  pcmplfin  30733  cnvordtrestixx  30765  ordtrest2NEWlem  30774  indval  30881  esumpfinvallem  30942  sigagenss  31017  ddemeas  31104  brae  31109  dya2iocival  31140  dya2iocnei  31149  dya2iocuni  31150  omsf  31163  oddpwdc  31221  bnj934  31815  spthcycl  31978  derangenlem  32020  subfacval2  32036  kur14  32065  sat1el2xp  32228  fmlasucdisj  32248  satfun  32260  lediv2aALT  32522  dford5  32559  faclim2  32582  funpsstri  32610  dftrpred3g  32675  soseq  32699  wsuclem  32715  fprlem1  32740  fpr1  32742  frrlem15  32745  frr1  32747  elno  32756  nosepon  32775  noextenddif  32778  sltsolem1  32783  nosepne  32788  nolt02o  32802  sltnle  32835  sleloe  32836  sletri3  32837  hfelhf  33245  elicc3  33268  nn0prpwlem  33273  nn0prpw  33274  isfne  33290  onsuct0  33392  nndivsub  33408  bj-nnfbit  33869  bj-restsnss  33986  bj-restsnss2  33987  bj-restuni2  34001  topdifinffinlem  34172  iooelexlt  34187  relowlssretop  34188  rdgeqoa  34195  finorwe  34207  nlpineqsn  34233  pibt2  34242  wl-sbcom2d-lem1  34339  wl-sbcom2d  34341  wl-ax11-lem6  34366  curf  34414  finixpnum  34421  ltflcei  34424  leceifl  34425  cos2h  34427  matunitlindflem1  34432  matunitlindflem2  34433  matunitlindf  34434  ptrecube  34436  poimirlem6  34442  poimirlem7  34443  poimirlem10  34446  poimirlem11  34447  poimirlem27  34463  poimirlem29  34465  poimirlem30  34466  poimirlem31  34467  poimirlem32  34468  mblfinlem3  34475  mblfinlem4  34476  ismblfin  34477  ovoliunnfl  34478  voliunnfl  34480  volsupnfl  34481  cnambfre  34484  itg2addnclem2  34488  itg2addnc  34490  itg2gt0cn  34491  ftc1anclem1  34511  ftc1anclem4  34514  ftc1anclem6  34516  ftc1anclem7  34517  ftc1anc  34519  unirep  34533  opelopab3  34537  fvopabf4g  34541  indexa  34553  filbcmb  34560  incsequz2  34569  metf1o  34575  sstotbnd3  34599  isbnd2  34606  bndss  34609  ismtycnv  34625  iccbnd  34663  exidreslem  34700  exidresid  34702  ghomco  34714  isdivrngo  34773  isdrngo2  34781  rngoisocnv  34804  riscer  34811  crngohomfo  34829  unichnidl  34854  maxidlmax  34866  igenmin  34887  exmid2  34922  orel  34925  brcosscnvcoss  35223  brssr  35285  brdmqss  35425  prtlem16  35549  paddss1  36497  paddss2  36498  paddss12  36499  pclfinN  36580  erngmul-rN  37494  mapdordlem2  38317  addsubeq4com  38701  dvdsexpim  38716  renegadd  38737  rersubcl  38744  repncan3  38749  readdsub  38750  renpncan3  38755  resubdi  38760  ismrc  38796  nacsfg  38800  isnacs3  38805  incssnn0  38806  mzpclall  38822  lerabdioph  38900  ltrabdioph  38903  eldioph4b  38906  jm2.17b  39056  congrep  39068  lnr2i  39214  ontric3g  39386  nndomog  39395  brnonrel  39447  enrelmap  39841  enrelmapr  39842  rcompleq  39868  isotone1  39896  isotone2  39897  prmgrpsimpgd  40184  radcnvrat  40197  expgrowth  40218  bcc0  40223  binomcxplemnn0  40232  2sbc6g  40298  2sbc5g  40299  ordpss  40335  addrcom  40359  3impcombi  40703  sspwimp  40804  sspwimpVD  40805  ax6e2ndeqALT  40817  iunconnlem2  40821  sineq0ALT  40823  nsstr  40913  iunmapsn  41033  ssfiunibd  41130  fmul01  41416  lptre2pt  41476  stoweidlem34  41875  dirkeritg  41943  fourierdlem73  42020  smfsuplem1  42641  smfinflem  42647  sigarac  42665  or2expropbi  42799  euoreqb  42838  2reu3  42839  2reuimp  42844  dfatelrn  42860  afv0nbfvbi  42880  dmfcoafv  42904  dfatcolem  42984  cnambpcma  43024  ltnltne  43029  fzoopth  43057  elmod2  43060  ichreuopeq  43131  sprsymrelfolem2  43151  sprsymrelf1  43154  prproropf1olem4  43164  poprelb  43182  reuopreuprim  43184  fmtnofac2lem  43226  prmdvdsfmtnof1lem2  43243  proththd  43275  opoeALTV  43344  opeoALTV  43345  epoo  43364  evenprm2  43375  gbegt5  43422  sbgoldbaltlem2  43441  nnsum4primeseven  43461  nnsum4primesevenALTV  43462  bgoldbtbndlem4  43469  bgoldbtbnd  43470  isomuspgrlem2d  43492  isomgrsym  43497  isomgrsymb  43498  uspgrsprfo  43519  submgmcl  43557  resmgmhm2b  43563  isassintop  43609  rnghmval  43654  isrngisom  43659  c0snghm  43679  zrrnghm  43680  2zrngamgm  43702  rnghmsubcsetclem2  43739  rhmsubcsetclem2  43785  rhmsubcrngclem1  43790  rhmsubcrngclem2  43791  funcringcsetcALTV2lem9  43807  funcringcsetclem9ALTV  43830  rhmsubclem4  43852  rhmsubcALTVlem4  43870  cbvmpox2  43876  nn0sumltlt  43890  gsumlsscl  43925  ply1mulgsumlem1  43934  lincvalpr  43967  lincdifsn  43973  linc1  43974  lincellss  43975  islinindfiss  43999  islindeps  44002  lincresunit2  44027  islininds2  44033  lmod1zr  44042  ltsubadd2b  44066  zgtp1leeq  44071  logblt1b  44119  blengt1fldiv2p1  44148  nn0sumshdiglemB  44175  line2  44234  itsclc0yqe  44243  itscnhlinecirc02p  44267  setrec2lem2  44291  aacllem  44396