Theorem ancom 460

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 459	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜓 ∧ 𝜑))
2		pm3.22 459	. 2 ⊢ ((𝜓 ∧ 𝜑) → (𝜑 ∧ 𝜓))
3	1, 2	impbii 209	1 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜓 ∧ 𝜑))

Syntax hints:   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  ancomd  461  biancomi  462  biancomd  463  ancomst  464  pm4.71r  558  pm5.32ri  575  pm5.32rd  578  an2anr  637  bianassc  644  an12  646  an13  648  an42  658  andir  1011  cases2  1048  dfifp6  1069  ifpn  1074  4anpull2  1363  excxor  1518  cador  1610  cadcoma  1614  exancom  1863  19.42v  1955  19.42  2244  sbel2x  2478  eu6  2574  moanmo  2622  2eu3  2654  2eu7  2658  2eu8  2659  eq2tri  2798  r19.42v  3169  rexcomf  3276  rabswap  3398  spc2ed  3543  euxfr2w  3666  euxfr2  3668  rmo4  3676  reu8  3679  rmo3f  3680  reuxfrd  3694  rmo3  3827  difin2  4241  rcompleq  4245  euelss  4272  ssunsn  4771  uniprg  4866  inuni  5291  eqvinop  5440  elxp2  5655  opeliun2xp  5699  elvvv  5707  brinxp2  5709  dmuni  5869  imadmrn  6035  asymref2  6080  cnvopab  6100  cnvxp  6121  xpdifid  6132  cnvcnvsn  6183  opswap  6193  mptpreima  6202  xpco  6253  dfpo2  6260  fncnv  6571  fnres  6625  mptfnf  6633  dff1o2  6785  f13dfv  7229  fliftcnv  7266  isoini  7293  elrnmpores  7505  ndmovcom  7554  uniuni  7716  opabex3rd  7919  mptmpoopabbrd  8033  fsplit  8067  brtpos  8185  tposmpo  8213  oaord  8482  nnaord  8555  naddasslem1  8630  naddasslem2  8631  brinxper  8673  pmex  8778  mapsnend  8983  snmapen  8985  xpsnen  8999  xpcomco  9005  elfi2  9327  supmo  9365  infmo  9410  frind  9674  cp  9815  dfac5lem1  10045  dfac5lem2  10046  dfac2b  10053  kmlem3  10075  cflim3  10184  brdom7disj  10453  brdom6disj  10454  recmulnq  10887  lesub0  11667  wloglei  11682  creur  12153  indstr  12866  xmulcom  13218  xmulneg1  13221  xmulf  13224  iccneg  13425  fzrev  13541  injresinj  13746  rediv  15093  imdiv  15100  lenegsq  15283  o1lo1  15499  fsumcom2  15736  fsumcom  15737  fprodcom2  15949  fprodcom  15950  divalglem10  16371  smueqlem  16459  gcdcom  16482  lcmcom  16562  isprm2  16651  isprm7  16678  infpn2  16884  imasleval  17505  dfiso3  17740  posglbmo  18376  odulatb  18400  oduclatb  18473  oppgid  19331  gsumcom  19952  gsumcom3  19953  dfrhm2  20454  xrsdsreclb  21394  opsrtoslem1  22033  psdmvr  22135  madutpos  22607  fvmptnn04if  22814  ntreq0  23042  ist0-3  23310  txkgen  23617  trfil2  23852  flimrest  23948  blres  24396  metrest  24489  restmetu  24535  elii1  24902  isclmp  25064  evthicc2  25427  ovolfcl  25433  dyaddisj  25563  iblpos  25760  itgposval  25763  ditgsplit  25828  itgsubst  26016  sincosq3sgn  26464  cos11  26497  dvdsflsumcom  27151  fsumvma  27176  logfaclbnd  27185  dchrelbas3  27201  lgsdi  27297  lgsquadlem3  27345  2lgslem1a  27354  lestri3  27719  ltsrec  27793  istrkg2ld  28528  tgjustf  28541  tgcgr4  28599  mirreu3  28722  hpgcom  28835  colhp  28838  dfcgra2  28898  nbgrel  29409  nbgrsym  29432  wlkson  29723  dfpth2  29797  isspthonpth  29817  usgr2pth0  29833  wwlksnextinj  29967  elwspths2spth  30038  rusgrnumwwlkl1  30039  clwwlknclwwlkdifnum  30050  clwwlkn1  30111  clwwlkn2  30114  iseupthf1o  30272  eupth2lem2  30289  frgrncvvdeqlem2  30370  fusgr2wsp2nb  30404  fusgreg2wsp  30406  frgrreg  30464  frgrregord013  30465  h2hcau  31050  nmopub  31979  nmfnleub  31996  chrelati  32435  cvexchlem  32439  mdsymlem8  32481  sumdmdii  32486  13an22anass  32533  2reucom  32549  reuxfrdf  32560  dmrab  32566  difrab2  32567  ressupprn  32763  2ndpreima  32781  fpwrelmapffslem  32805  xrofsup  32840  sgn3da  32907  mgccnv  33059  pmtrprfv2  33149  smatrcl  33940  cnvordtrestixx  34057  issgon  34267  eulerpartlemr  34518  eulerpartlemgvv  34520  ballotlem2  34633  oddprm2  34799  bnj257  34850  bnj545  35037  bnj594  35054  nfan1c  35215  satfv0  35540  satfvsuclem1  35541  dfdm5  35955  dfrn5  35956  elima4  35958  elfix  36083  dffix2  36085  brimg  36117  lemsuccf  36121  dfrecs2  36132  dfrdg4  36133  cgrcomlr  36180  ofscom  36189  btwnexch  36207  fscgr  36262  bj-df-ifc  36845  bj-axseprep  37381  bj-dfmpoa  37430  bj-eldiag  37490  bj-imdirco  37504  bj-ccinftydisj  37527  mptsnunlem  37654  topdifinffinlem  37663  fvineqsneq  37728  wl-cases2-dnf  37837  fin2solem  37927  poimirlem26  37967  poimirlem30  37971  poimirlem32  37973  ftc1anclem6  38019  ftc1anc  38022  heibor1  38131  isdrngo3  38280  isdmn3  38395  anan  38556  br1cnvinxp  38580  raldmqseu  38686  inxpxrn  38739  prtlem70  39303  lrelat  39460  islshpat  39463  atlrelat1  39767  ishlat2  39799  cdlemb3  41052  diblsmopel  41617  dicelval3  41626  diclspsn  41640  uzindd  42417  3factsumint2  42461  3factsumint3  42462  3factsumint  42464  fimgmcyc  42979  eu6w  43109  fz1eqin  43201  diophrex  43207  fphpd  43244  fzneg  43410  expdioph  43451  dford4  43457  lnr2i  43544  fgraphopab  43631  omge2  43726  oadif1lem  43807  oadif1  43808  ifpancor  43891  ifpidg  43918  ifpid2g  43920  ifpid1g  43921  ifpim23g  43922  rp-fakeoranass  43941  minregex  43961  dfid7  44039  dfrtrcl5  44056  relexp0eq  44128  fsovrfovd  44436  rr-grothprimbi  44722  uunT1p1  45207  uun132p1  45212  un2122  45216  uun2131p1  45218  uunT12p1  45226  uunT12p2  45227  uunT12p3  45228  uun2221  45239  uun2221p1  45240  uun2221p2  45241  3impdirp1  45242  ancomstVD  45291  icccncfext  46315  dvnmul  46371  dvmptfprodlem  46372  dvnprodlem2  46375  fourierdlem42  46577  fourierdlem83  46617  f1cof1b  47525  2reu3  47558  2reu7  47559  2reu8  47560  2reuimp0  47562  ndmaovcom  47653  an4com24  47716  4an21  47718  sprvalpwn0  47943  prpair  47961  prproropf1olem0  47962  clnbgrel  48304  clnbgrsym  48314  2zrngnmrid  48732  rrx2linest  49218  pm5.32dav  49269  resinsnALT  49348  catcinv  49874  thincsect2  49943  lmdfval  50124  cmdfval  50125