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  3169  rexcomf  3277  rabswap  3415  spc2ed  3567  euxfr2w  3691  euxfr2  3693  rmo4  3701  reu8  3704  rmo3f  3705  reuxfrd  3719  rmo3  3852  difin2  4264  rcompleq  4268  euelss  4295  ssunsn  4792  uniprg  4887  inuni  5305  eqvinop  5447  elxp2  5662  opeliun2xp  5706  elvvv  5714  brinxp2  5716  dmuni  5878  imadmrn  6041  asymref2  6090  cnvopab  6110  cnvxp  6130  xpdifid  6141  cnvcnvsn  6192  opswap  6202  mptpreima  6211  xpco  6262  dfpo2  6269  fncnv  6589  fnres  6645  mptfnf  6653  dff1o2  6805  f13dfv  7249  fliftcnv  7286  isoini  7313  elrnmpores  7527  ndmovcom  7576  uniuni  7738  opabex3rd  7945  mptmpoopabbrd  8059  mptmpoopabbrdOLD  8060  mptmpoopabbrdOLDOLD  8062  fsplit  8096  brtpos  8214  tposmpo  8242  oaord  8511  nnaord  8583  naddasslem1  8658  naddasslem2  8659  brinxper  8700  pmex  8804  mapsnend  9007  snmapen  9009  xpsnen  9025  xpcomco  9031  elfi2  9365  supmo  9403  infmo  9448  frind  9703  cp  9844  dfac5lem1  10076  dfac5lem2  10077  dfac2b  10084  kmlem3  10106  cflim3  10215  brdom7disj  10484  brdom6disj  10485  recmulnq  10917  lesub0  11695  wloglei  11710  creur  12180  indstr  12875  xmulcom  13226  xmulneg1  13229  xmulf  13232  iccneg  13433  fzrev  13548  injresinj  13749  rediv  15097  imdiv  15104  lenegsq  15287  o1lo1  15503  fsumcom2  15740  fsumcom  15741  fprodcom2  15950  fprodcom  15951  divalglem10  16372  smueqlem  16460  gcdcom  16483  lcmcom  16563  isprm2  16652  isprm7  16678  infpn2  16884  imasleval  17504  dfiso3  17735  posglbmo  18371  odulatb  18393  oduclatb  18466  oppgid  19288  gsumcom  19907  gsumcom3  19908  dfrhm2  20383  xrsdsreclb  21330  opsrtoslem1  21962  psdmvr  22056  madutpos  22529  fvmptnn04if  22736  ntreq0  22964  ist0-3  23232  txkgen  23539  trfil2  23774  flimrest  23870  blres  24319  metrest  24412  restmetu  24458  elii1  24831  isclmp  24997  evthicc2  25361  ovolfcl  25367  dyaddisj  25497  iblpos  25694  itgposval  25697  ditgsplit  25762  itgsubst  25956  sincosq3sgn  26409  cos11  26442  dvdsflsumcom  27098  fsumvma  27124  logfaclbnd  27133  dchrelbas3  27149  lgsdi  27245  lgsquadlem3  27293  2lgslem1a  27302  sletri3  27667  nocvxmin  27690  sltrec  27732  istrkg2ld  28387  tgjustf  28400  tgcgr4  28458  mirreu3  28581  hpgcom  28694  colhp  28697  dfcgra2  28757  nbgrel  29267  nbgrsym  29290  wlkson  29584  dfpth2  29659  isspthonpth  29679  usgr2pth0  29695  wwlksnextinj  29829  elwspths2spth  29897  rusgrnumwwlkl1  29898  clwwlknclwwlkdifnum  29909  clwwlkn1  29970  clwwlkn2  29973  iseupthf1o  30131  eupth2lem2  30148  frgrncvvdeqlem2  30229  fusgr2wsp2nb  30263  fusgreg2wsp  30265  frgrreg  30323  frgrregord013  30324  h2hcau  30908  nmopub  31837  nmfnleub  31854  chrelati  32293  cvexchlem  32297  mdsymlem8  32339  sumdmdii  32344  13an22anass  32393  2reucom  32409  reuxfrdf  32420  dmrab  32426  difrab2  32427  ressupprn  32613  2ndpreima  32631  fpwrelmapffslem  32655  xrofsup  32690  sgn3da  32759  mgccnv  32925  pmtrprfv2  33045  smatrcl  33786  cnvordtrestixx  33903  issgon  34113  eulerpartlemr  34365  eulerpartlemgvv  34367  ballotlem2  34480  oddprm2  34646  bnj257  34697  bnj545  34885  bnj594  34902  nfan1c  35063  satfv0  35345  satfvsuclem1  35346  dfdm5  35760  dfrn5  35761  elima4  35763  elfix  35891  dffix2  35893  brimg  35925  brsuccf  35929  dfrecs2  35938  dfrdg4  35939  cgrcomlr  35986  ofscom  35995  btwnexch  36013  fscgr  36068  bj-df-ifc  36568  bj-dfmpoa  37106  bj-eldiag  37164  bj-imdirco  37178  bj-ccinftydisj  37201  mptsnunlem  37326  topdifinffinlem  37335  fvineqsneq  37400  wl-cases2-dnf  37500  wl-ax11-lem4  37576  fin2solem  37600  poimirlem26  37640  poimirlem30  37644  poimirlem32  37646  ftc1anclem6  37692  ftc1anc  37695  heibor1  37804  isdrngo3  37953  isdmn3  38068  anan  38217  br1cnvinxp  38245  inxpxrn  38381  prtlem70  38850  lrelat  39007  islshpat  39010  atlrelat1  39314  ishlat2  39346  cdlemb3  40600  diblsmopel  41165  dicelval3  41174  diclspsn  41188  uzindd  41965  3factsumint2  42010  3factsumint3  42011  3factsumint  42013  fimgmcyc  42522  eu6w  42664  fz1eqin  42757  diophrex  42763  fphpd  42804  fzneg  42971  expdioph  43012  dford4  43018  lnr2i  43105  fgraphopab  43192  omge2  43287  oadif1lem  43368  oadif1  43369  ifpancor  43453  ifpidg  43480  ifpid2g  43482  ifpid1g  43483  ifpim23g  43484  rp-fakeoranass  43503  minregex  43523  dfid7  43601  dfrtrcl5  43618  relexp0eq  43690  fsovrfovd  43998  rr-grothprimbi  44284  uunT1p1  44770  uun132p1  44775  un2122  44779  uun2131p1  44781  uunT12p1  44789  uunT12p2  44790  uunT12p3  44791  uun2221  44802  uun2221p1  44803  uun2221p2  44804  3impdirp1  44805  ancomstVD  44854  icccncfext  45885  dvnmul  45941  dvmptfprodlem  45942  dvnprodlem2  45945  fourierdlem42  46147  fourierdlem83  46187  f1cof1b  47078  2reu3  47111  2reu7  47112  2reu8  47113  2reuimp0  47115  ndmaovcom  47206  an4com24  47269  4an21  47271  sprvalpwn0  47484  prpair  47502  prproropf1olem0  47503  clnbgrel  47829  clnbgrsym  47838  2zrngnmrid  48244  rrx2linest  48731  pm5.32dav  48782  resinsnALT  48861  catcinv  49388  thincsect2  49457  lmdfval  49638  cmdfval  49639