Theorem ancom 461

Description: Commutative law for conjunction. Theorem *4.3 of [WhiteheadRussell] p. 118. (Contributed by NM, 25-Jun-1998.) (Proof shortened by Wolf Lammen, 4-Nov-2012.)

Assertion

Ref	Expression
ancom	⊢ ((𝜑 ∧ 𝜓) ↔ (𝜓 ∧ 𝜑))

Proof of Theorem ancom

Step	Hyp	Ref	Expression
1		pm3.22 460	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜓 ∧ 𝜑))
2		pm3.22 460	. 2 ⊢ ((𝜓 ∧ 𝜑) → (𝜑 ∧ 𝜓))
3	1, 2	impbii 210	1 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜓 ∧ 𝜑))

Syntax hints:   ↔ wb 207   ∧ 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:  ancomd  462  biancomi  463  biancomd  464  ancomst  465  pm4.71r  563  pm5.32ri  580  pm5.32rd  583  an2anr  642  bianassc  649  an12  651  an13  653  an42  663  andir  1016  cases2  1053  dfifp6  1074  ifpn  1079  4anpull2  1368  excxor  1523  cador  1615  cadcoma  1619  exancom  1868  19.42v  1960  19.42  2248  sbel2x  2482  eu6  2578  moanmo  2626  2eu3  2657  2eu7  2661  2eu8  2662  eq2tri  2801  r19.42v  3171  rexcomf  3278  rabswap  3400  spc2ed  3539  euxfr2w  3661  euxfr2  3663  rmo4  3671  reu8  3674  rmo3f  3675  reuxfrd  3689  rmo3  3821  difin2  4229  rcompleq  4233  euelss  4260  ssunsn  4759  uniprg  4854  inuni  5278  eqvinop  5427  elxp2  5642  opeliun2xp  5686  elvvv  5694  brinxp2  5696  dmuni  5856  imadmrn  6022  asymref2  6067  cnvopab  6087  cnvxp  6108  xpdifid  6119  cnvcnvsn  6170  opswap  6180  mptpreima  6189  xpco  6240  dfpo2  6247  fncnv  6558  fnres  6612  mptfnf  6620  dff1o2  6772  f13dfv  7218  fliftcnv  7255  isoini  7282  elrnmpores  7494  ndmovcom  7543  uniuni  7705  opabex3rd  7908  mptmpoopabbrd  8022  fsplit  8056  brtpos  8175  tposmpo  8203  oaord  8472  nnaord  8545  naddasslem1  8620  naddasslem2  8621  brinxper  8663  pmex  8768  mapsnend  8973  snmapen  8975  xpsnen  8989  xpcomco  8995  elfi2  9317  supmo  9355  infmo  9400  frind  9665  cp  9806  dfac5lem1  10036  dfac5lem2  10037  dfac2b  10044  kmlem3  10066  cflim3  10175  brdom7disj  10444  brdom6disj  10445  recmulnq  10878  lesub0  11658  wloglei  11673  creur  12144  indstr  12857  xmulcom  13209  xmulneg1  13212  xmulf  13215  iccneg  13416  fzrev  13532  injresinj  13737  rediv  15084  imdiv  15091  lenegsq  15274  o1lo1  15490  fsumcom2  15727  fsumcom  15728  fprodcom2  15940  fprodcom  15941  divalglem10  16362  smueqlem  16450  gcdcom  16473  lcmcom  16553  isprm2  16642  isprm7  16669  infpn2  16875  imasleval  17496  dfiso3  17731  posglbmo  18367  odulatb  18391  oduclatb  18464  oppgid  19322  gsumcom  19943  gsumcom3  19944  dfrhm2  20445  xrsdsreclb  21389  opsrtoslem1  22031  psdmvr  22157  madutpos  22625  fvmptnn04if  22832  ntreq0  23060  ist0-3  23328  txkgen  23635  trfil2  23870  flimrest  23966  blres  24414  metrest  24507  restmetu  24553  elii1  24920  isclmp  25082  evthicc2  25445  ovolfcl  25451  dyaddisj  25581  iblpos  25778  itgposval  25781  ditgsplit  25846  itgsubst  26034  sincosq3sgn  26482  cos11  26515  dvdsflsumcom  27169  fsumvma  27194  logfaclbnd  27203  dchrelbas3  27219  lgsdi  27315  lgsquadlem3  27363  2lgslem1a  27372  lestri3  27737  ltsrec  27811  istrkg2ld  28546  tgjustf  28559  tgcgr4  28617  mirreu3  28740  hpgcom  28853  colhp  28856  dfcgra2  28916  nbgrel  29427  nbgrsym  29450  wlkson  29741  dfpth2  29815  isspthonpth  29835  usgr2pth0  29851  wwlksnextinj  29985  elwspths2spth  30056  rusgrnumwwlkl1  30057  clwwlknclwwlkdifnum  30068  clwwlkn1  30129  clwwlkn2  30132  iseupthf1o  30290  eupth2lem2  30307  frgrncvvdeqlem2  30388  fusgr2wsp2nb  30422  fusgreg2wsp  30424  frgrreg  30482  frgrregord013  30483  h2hcau  31068  nmopub  31997  nmfnleub  32014  chrelati  32453  cvexchlem  32457  mdsymlem8  32499  sumdmdii  32504  13an22anass  32551  2reucom  32567  reuxfrdf  32578  dmrab  32584  difrab2  32585  ififcom  32638  ressupprn  32782  2ndpreima  32800  fpwrelmapffslem  32824  xrofsup  32859  sgn3da  32926  mgccnv  33078  pmtrprfv2  33169  smatrcl  33980  cnvordtrestixx  34097  issgon  34307  eulerpartlemr  34558  eulerpartlemgvv  34560  ballotlem2  34673  oddprm2  34839  bnj257  34890  bnj545  35077  bnj594  35094  nfan1c  35255  satfv0  35586  satfvsuclem1  35587  dfdm5  36001  dfrn5  36002  elima4  36004  elfix  36129  dffix2  36131  brimg  36163  lemsuccf  36167  dfrecs2  36178  dfrdg4  36179  cgrcomlr  36226  ofscom  36235  btwnexch  36253  fscgr  36308  bj-df-ifc  36891  bj-axseprep  37427  bj-dfmpoa  37476  bj-eldiag  37536  bj-imdirco  37550  bj-ccinftydisj  37573  mptsnunlem  37700  topdifinffinlem  37709  fvineqsneq  37774  wl-cases2-dnf  37883  fin2solem  37973  poimirlem26  38013  poimirlem30  38017  poimirlem32  38019  ftc1anclem6  38065  ftc1anc  38068  heibor1  38177  isdrngo3  38326  isdmn3  38441  anan  38602  br1cnvinxp  38626  raldmqseu  38732  inxpxrn  38785  prtlem70  39349  lrelat  39506  islshpat  39509  atlrelat1  39813  ishlat2  39845  cdlemb3  41098  diblsmopel  41663  dicelval3  41672  diclspsn  41686  uzindd  42463  3factsumint2  42507  3factsumint3  42508  3factsumint  42510  fimgmcyc  43020  eu6w  43126  fz1eqin  43218  diophrex  43224  fphpd  43261  fzneg  43427  expdioph  43468  dford4  43474  lnr2i  43561  fgraphopab  43648  omge2  43743  oadif1lem  43824  oadif1  43825  ifpancor  43908  ifpidg  43935  ifpid2g  43937  ifpid1g  43938  ifpim23g  43939  rp-fakeoranass  43958  minregex  43978  dfid7  44056  dfrtrcl5  44073  relexp0eq  44145  fsovrfovd  44453  rr-grothprimbi  44739  uunT1p1  45224  uun132p1  45229  un2122  45233  uun2131p1  45235  uunT12p1  45243  uunT12p2  45244  uunT12p3  45245  uun2221  45256  uun2221p1  45257  uun2221p2  45258  3impdirp1  45259  ancomstVD  45308  icccncfext  46330  dvnmul  46386  dvmptfprodlem  46387  dvnprodlem2  46390  fourierdlem42  46592  fourierdlem83  46632  f1cof1b  47540  2reu3  47573  2reu7  47574  2reu8  47575  2reuimp0  47577  ndmaovcom  47668  an4com24  47731  4an21  47733  sprvalpwn0  47958  prpair  47976  prproropf1olem0  47977  clnbgrel  48319  clnbgrsym  48329  2zrngnmrid  48747  rrx2linest  49233  pm5.32dav  49284  resinsnALT  49363  catcinv  49889  thincsect2  49958  lmdfval  50139  cmdfval  50140