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  636  bianassc  643  an12  645  an13  647  an42  657  andir  1010  cases2  1047  dfifp6  1068  ifpn  1073  4anpull2  1362  excxor  1517  cador  1609  cadcoma  1613  exancom  1862  19.42v  1954  19.42  2243  sbel2x  2478  eu6  2574  moanmo  2622  2eu3  2654  2eu7  2658  2eu8  2659  eq2tri  2798  r19.42v  3168  rexcomf  3275  rabswap  3408  spc2ed  3555  euxfr2w  3678  euxfr2  3680  rmo4  3688  reu8  3691  rmo3f  3692  reuxfrd  3706  rmo3  3839  difin2  4253  rcompleq  4257  euelss  4284  ssunsn  4784  uniprg  4879  inuni  5295  eqvinop  5435  elxp2  5648  opeliun2xp  5692  elvvv  5700  brinxp2  5702  dmuni  5863  imadmrn  6029  asymref2  6074  cnvopab  6094  cnvxp  6115  xpdifid  6126  cnvcnvsn  6177  opswap  6187  mptpreima  6196  xpco  6247  dfpo2  6254  fncnv  6565  fnres  6619  mptfnf  6627  dff1o2  6779  f13dfv  7220  fliftcnv  7257  isoini  7284  elrnmpores  7496  ndmovcom  7545  uniuni  7707  opabex3rd  7910  mptmpoopabbrd  8024  mptmpoopabbrdOLD  8025  fsplit  8059  brtpos  8177  tposmpo  8205  oaord  8474  nnaord  8547  naddasslem1  8622  naddasslem2  8623  brinxper  8664  pmex  8768  mapsnend  8973  snmapen  8975  xpsnen  8989  xpcomco  8995  elfi2  9317  supmo  9355  infmo  9400  frind  9662  cp  9803  dfac5lem1  10033  dfac5lem2  10034  dfac2b  10041  kmlem3  10063  cflim3  10172  brdom7disj  10441  brdom6disj  10442  recmulnq  10875  lesub0  11654  wloglei  11669  creur  12139  indstr  12829  xmulcom  13181  xmulneg1  13184  xmulf  13187  iccneg  13388  fzrev  13503  injresinj  13707  rediv  15054  imdiv  15061  lenegsq  15244  o1lo1  15460  fsumcom2  15697  fsumcom  15698  fprodcom2  15907  fprodcom  15908  divalglem10  16329  smueqlem  16417  gcdcom  16440  lcmcom  16520  isprm2  16609  isprm7  16635  infpn2  16841  imasleval  17462  dfiso3  17697  posglbmo  18333  odulatb  18357  oduclatb  18430  oppgid  19285  gsumcom  19906  gsumcom3  19907  dfrhm2  20410  xrsdsreclb  21368  opsrtoslem1  22010  psdmvr  22112  madutpos  22586  fvmptnn04if  22793  ntreq0  23021  ist0-3  23289  txkgen  23596  trfil2  23831  flimrest  23927  blres  24375  metrest  24468  restmetu  24514  elii1  24887  isclmp  25053  evthicc2  25417  ovolfcl  25423  dyaddisj  25553  iblpos  25750  itgposval  25753  ditgsplit  25818  itgsubst  26012  sincosq3sgn  26465  cos11  26498  dvdsflsumcom  27154  fsumvma  27180  logfaclbnd  27189  dchrelbas3  27205  lgsdi  27301  lgsquadlem3  27349  2lgslem1a  27358  lestri3  27723  ltsrec  27797  istrkg2ld  28532  tgjustf  28545  tgcgr4  28603  mirreu3  28726  hpgcom  28839  colhp  28842  dfcgra2  28902  nbgrel  29413  nbgrsym  29436  wlkson  29728  dfpth2  29802  isspthonpth  29822  usgr2pth0  29838  wwlksnextinj  29972  elwspths2spth  30043  rusgrnumwwlkl1  30044  clwwlknclwwlkdifnum  30055  clwwlkn1  30116  clwwlkn2  30119  iseupthf1o  30277  eupth2lem2  30294  frgrncvvdeqlem2  30375  fusgr2wsp2nb  30409  fusgreg2wsp  30411  frgrreg  30469  frgrregord013  30470  h2hcau  31054  nmopub  31983  nmfnleub  32000  chrelati  32439  cvexchlem  32443  mdsymlem8  32485  sumdmdii  32490  13an22anass  32538  2reucom  32554  reuxfrdf  32565  dmrab  32571  difrab2  32572  ressupprn  32769  2ndpreima  32787  fpwrelmapffslem  32811  xrofsup  32847  sgn3da  32915  mgccnv  33081  pmtrprfv2  33170  smatrcl  33953  cnvordtrestixx  34070  issgon  34280  eulerpartlemr  34531  eulerpartlemgvv  34533  ballotlem2  34646  oddprm2  34812  bnj257  34863  bnj545  35051  bnj594  35068  nfan1c  35229  satfv0  35552  satfvsuclem1  35553  dfdm5  35967  dfrn5  35968  elima4  35970  elfix  36095  dffix2  36097  brimg  36129  lemsuccf  36133  dfrecs2  36144  dfrdg4  36145  cgrcomlr  36192  ofscom  36201  btwnexch  36219  fscgr  36274  bj-df-ifc  36780  bj-dfmpoa  37323  bj-eldiag  37381  bj-imdirco  37395  bj-ccinftydisj  37418  mptsnunlem  37543  topdifinffinlem  37552  fvineqsneq  37617  wl-cases2-dnf  37717  fin2solem  37807  poimirlem26  37847  poimirlem30  37851  poimirlem32  37853  ftc1anclem6  37899  ftc1anc  37902  heibor1  38011  isdrngo3  38160  isdmn3  38275  anan  38431  br1cnvinxp  38454  inxpxrn  38603  prtlem70  39117  lrelat  39274  islshpat  39277  atlrelat1  39581  ishlat2  39613  cdlemb3  40866  diblsmopel  41431  dicelval3  41440  diclspsn  41454  uzindd  42231  3factsumint2  42276  3factsumint3  42277  3factsumint  42279  fimgmcyc  42789  eu6w  42919  fz1eqin  43011  diophrex  43017  fphpd  43058  fzneg  43224  expdioph  43265  dford4  43271  lnr2i  43358  fgraphopab  43445  omge2  43540  oadif1lem  43621  oadif1  43622  ifpancor  43705  ifpidg  43732  ifpid2g  43734  ifpid1g  43735  ifpim23g  43736  rp-fakeoranass  43755  minregex  43775  dfid7  43853  dfrtrcl5  43870  relexp0eq  43942  fsovrfovd  44250  rr-grothprimbi  44536  uunT1p1  45021  uun132p1  45026  un2122  45030  uun2131p1  45032  uunT12p1  45040  uunT12p2  45041  uunT12p3  45042  uun2221  45053  uun2221p1  45054  uun2221p2  45055  3impdirp1  45056  ancomstVD  45105  icccncfext  46131  dvnmul  46187  dvmptfprodlem  46188  dvnprodlem2  46191  fourierdlem42  46393  fourierdlem83  46433  f1cof1b  47323  2reu3  47356  2reu7  47357  2reu8  47358  2reuimp0  47360  ndmaovcom  47451  an4com24  47514  4an21  47516  sprvalpwn0  47729  prpair  47747  prproropf1olem0  47748  clnbgrel  48074  clnbgrsym  48084  2zrngnmrid  48502  rrx2linest  48988  pm5.32dav  49039  resinsnALT  49118  catcinv  49644  thincsect2  49713  lmdfval  49894  cmdfval  49895