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  1516  cador  1608  cadcoma  1612  exancom  1861  19.42v  1953  19.42  2237  sbel2x  2472  eu6  2567  moanmo  2615  2eu3  2647  2eu7  2651  2eu8  2652  eq2tri  2791  r19.42v  3161  rexcomf  3269  rabswap  3406  spc2ed  3558  euxfr2w  3682  euxfr2  3684  rmo4  3692  reu8  3695  rmo3f  3696  reuxfrd  3710  rmo3  3843  difin2  4254  rcompleq  4258  euelss  4285  ssunsn  4782  uniprg  4877  inuni  5292  eqvinop  5434  elxp2  5647  opeliun2xp  5691  elvvv  5699  brinxp2  5701  dmuni  5861  imadmrn  6025  asymref2  6070  cnvopab  6090  cnvxp  6110  xpdifid  6121  cnvcnvsn  6172  opswap  6182  mptpreima  6191  xpco  6241  dfpo2  6248  fncnv  6559  fnres  6613  mptfnf  6621  dff1o2  6773  f13dfv  7215  fliftcnv  7252  isoini  7279  elrnmpores  7491  ndmovcom  7540  uniuni  7702  opabex3rd  7908  mptmpoopabbrd  8022  mptmpoopabbrdOLD  8023  fsplit  8057  brtpos  8175  tposmpo  8203  oaord  8472  nnaord  8544  naddasslem1  8619  naddasslem2  8620  brinxper  8661  pmex  8765  mapsnend  8968  snmapen  8970  xpsnen  8985  xpcomco  8991  elfi2  9323  supmo  9361  infmo  9406  frind  9665  cp  9806  dfac5lem1  10036  dfac5lem2  10037  dfac2b  10044  kmlem3  10066  cflim3  10175  brdom7disj  10444  brdom6disj  10445  recmulnq  10877  lesub0  11655  wloglei  11670  creur  12140  indstr  12835  xmulcom  13186  xmulneg1  13189  xmulf  13192  iccneg  13393  fzrev  13508  injresinj  13709  rediv  15056  imdiv  15063  lenegsq  15246  o1lo1  15462  fsumcom2  15699  fsumcom  15700  fprodcom2  15909  fprodcom  15910  divalglem10  16331  smueqlem  16419  gcdcom  16442  lcmcom  16522  isprm2  16611  isprm7  16637  infpn2  16843  imasleval  17463  dfiso3  17698  posglbmo  18334  odulatb  18358  oduclatb  18431  oppgid  19253  gsumcom  19874  gsumcom3  19875  dfrhm2  20377  xrsdsreclb  21338  opsrtoslem1  21978  psdmvr  22072  madutpos  22545  fvmptnn04if  22752  ntreq0  22980  ist0-3  23248  txkgen  23555  trfil2  23790  flimrest  23886  blres  24335  metrest  24428  restmetu  24474  elii1  24847  isclmp  25013  evthicc2  25377  ovolfcl  25383  dyaddisj  25513  iblpos  25710  itgposval  25713  ditgsplit  25778  itgsubst  25972  sincosq3sgn  26425  cos11  26458  dvdsflsumcom  27114  fsumvma  27140  logfaclbnd  27149  dchrelbas3  27165  lgsdi  27261  lgsquadlem3  27309  2lgslem1a  27318  sletri3  27683  sltrec  27750  istrkg2ld  28423  tgjustf  28436  tgcgr4  28494  mirreu3  28617  hpgcom  28730  colhp  28733  dfcgra2  28793  nbgrel  29303  nbgrsym  29326  wlkson  29618  dfpth2  29692  isspthonpth  29712  usgr2pth0  29728  wwlksnextinj  29862  elwspths2spth  29930  rusgrnumwwlkl1  29931  clwwlknclwwlkdifnum  29942  clwwlkn1  30003  clwwlkn2  30006  iseupthf1o  30164  eupth2lem2  30181  frgrncvvdeqlem2  30262  fusgr2wsp2nb  30296  fusgreg2wsp  30298  frgrreg  30356  frgrregord013  30357  h2hcau  30941  nmopub  31870  nmfnleub  31887  chrelati  32326  cvexchlem  32330  mdsymlem8  32372  sumdmdii  32377  13an22anass  32426  2reucom  32442  reuxfrdf  32453  dmrab  32459  difrab2  32460  ressupprn  32646  2ndpreima  32664  fpwrelmapffslem  32688  xrofsup  32723  sgn3da  32792  mgccnv  32954  pmtrprfv2  33043  smatrcl  33765  cnvordtrestixx  33882  issgon  34092  eulerpartlemr  34344  eulerpartlemgvv  34346  ballotlem2  34459  oddprm2  34625  bnj257  34676  bnj545  34864  bnj594  34881  nfan1c  35042  satfv0  35333  satfvsuclem1  35334  dfdm5  35748  dfrn5  35749  elima4  35751  elfix  35879  dffix2  35881  brimg  35913  brsuccf  35917  dfrecs2  35926  dfrdg4  35927  cgrcomlr  35974  ofscom  35983  btwnexch  36001  fscgr  36056  bj-df-ifc  36556  bj-dfmpoa  37094  bj-eldiag  37152  bj-imdirco  37166  bj-ccinftydisj  37189  mptsnunlem  37314  topdifinffinlem  37323  fvineqsneq  37388  wl-cases2-dnf  37488  wl-ax11-lem4  37564  fin2solem  37588  poimirlem26  37628  poimirlem30  37632  poimirlem32  37634  ftc1anclem6  37680  ftc1anc  37683  heibor1  37792  isdrngo3  37941  isdmn3  38056  anan  38205  br1cnvinxp  38233  inxpxrn  38369  prtlem70  38838  lrelat  38995  islshpat  38998  atlrelat1  39302  ishlat2  39334  cdlemb3  40588  diblsmopel  41153  dicelval3  41162  diclspsn  41176  uzindd  41953  3factsumint2  41998  3factsumint3  41999  3factsumint  42001  fimgmcyc  42510  eu6w  42652  fz1eqin  42745  diophrex  42751  fphpd  42792  fzneg  42958  expdioph  42999  dford4  43005  lnr2i  43092  fgraphopab  43179  omge2  43274  oadif1lem  43355  oadif1  43356  ifpancor  43440  ifpidg  43467  ifpid2g  43469  ifpid1g  43470  ifpim23g  43471  rp-fakeoranass  43490  minregex  43510  dfid7  43588  dfrtrcl5  43605  relexp0eq  43677  fsovrfovd  43985  rr-grothprimbi  44271  uunT1p1  44757  uun132p1  44762  un2122  44766  uun2131p1  44768  uunT12p1  44776  uunT12p2  44777  uunT12p3  44778  uun2221  44789  uun2221p1  44790  uun2221p2  44791  3impdirp1  44792  ancomstVD  44841  icccncfext  45872  dvnmul  45928  dvmptfprodlem  45929  dvnprodlem2  45932  fourierdlem42  46134  fourierdlem83  46174  f1cof1b  47065  2reu3  47098  2reu7  47099  2reu8  47100  2reuimp0  47102  ndmaovcom  47193  an4com24  47256  4an21  47258  sprvalpwn0  47471  prpair  47489  prproropf1olem0  47490  clnbgrel  47816  clnbgrsym  47826  2zrngnmrid  48244  rrx2linest  48731  pm5.32dav  48782  resinsnALT  48861  catcinv  49388  thincsect2  49457  lmdfval  49638  cmdfval  49639