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 208	1 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜓 ∧ 𝜑))

Syntax hints:   ↔ wb 205   ∧ 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 206  df-an 397

This theorem is referenced by:  ancomd  462  biancomi  463  biancomd  464  ancomst  465  pm4.71r  559  pm5.32ri  576  pm5.32rd  578  an2anr  635  bianassc  641  an12  643  an13  645  an42  655  andir  1007  cases2  1046  dfifp6  1067  ifpn  1072  excxor  1515  cador  1609  cadcoma  1613  exancom  1864  19.42v  1957  19.42  2229  sbel2x  2472  eu6  2567  moanmo  2617  2eu3  2648  2eu7  2652  2eu8  2653  eq2tri  2798  r19.42v  3183  rexcomf  3284  rabswap  3414  spc2ed  3561  euxfr2w  3681  euxfr2  3683  rmo4  3691  reu8  3694  rmo3f  3695  reuxfrd  3709  rmo3  3848  difin2  4256  rcompleq  4260  euelss  4286  ssunsn  4793  uniprg  4887  inuni  5305  eqvinop  5449  elxp2  5662  elvvv  5712  brinxp2  5714  dmuni  5875  imadmrn  6028  asymref2  6076  cnvxp  6114  xpdifid  6125  cnvcnvsn  6176  opswap  6186  mptpreima  6195  xpco  6246  dfpo2  6253  fncnv  6579  fnres  6633  mptfnf  6641  dff1o2  6794  f13dfv  7225  fliftcnv  7261  isoini  7288  elrnmpores  7498  ndmovcom  7546  uniuni  7701  opabex3rd  7904  mptmpoopabbrd  8018  mptmpoopabbrdOLD  8020  fsplit  8054  brtpos  8171  tposmpo  8199  oaord  8499  nnaord  8571  naddasslem1  8645  naddasslem2  8646  pmex  8777  mapsnend  8987  snmapen  8989  xpsnen  9006  xpcomco  9013  elfi2  9359  supmo  9397  infmo  9440  frind  9695  cp  9836  dfac5lem1  10068  dfac5lem2  10069  dfac2b  10075  kmlem3  10097  cflim3  10207  brdom7disj  10476  brdom6disj  10477  recmulnq  10909  lesub0  11681  wloglei  11696  creur  12156  indstr  12850  xmulcom  13195  xmulneg1  13198  xmulf  13201  iccneg  13399  fzrev  13514  injresinj  13703  rediv  15028  imdiv  15035  lenegsq  15217  o1lo1  15431  fsumcom2  15670  fsumcom  15671  fprodcom2  15878  fprodcom  15879  divalglem10  16295  smueqlem  16381  gcdcom  16404  lcmcom  16480  isprm2  16569  isprm7  16595  infpn2  16796  imasleval  17437  dfiso3  17670  posglbmo  18315  odulatb  18337  oduclatb  18410  oppgid  19151  gsumcom  19768  gsumcom3  19769  dfrhm2  20164  xrsdsreclb  20881  opsrtoslem1  21499  madutpos  22028  fvmptnn04if  22235  ntreq0  22465  ist0-3  22733  txkgen  23040  trfil2  23275  flimrest  23371  blres  23821  metrest  23917  restmetu  23963  elii1  24335  isclmp  24497  evthicc2  24861  ovolfcl  24867  dyaddisj  24997  iblpos  25194  itgposval  25197  ditgsplit  25262  itgsubst  25450  sincosq3sgn  25894  cos11  25926  dvdsflsumcom  26574  fsumvma  26598  logfaclbnd  26607  dchrelbas3  26623  lgsdi  26719  lgsquadlem3  26767  2lgslem1a  26776  sletri3  27140  nocvxmin  27161  sltrec  27202  istrkg2ld  27465  tgjustf  27478  tgcgr4  27536  mirreu3  27659  hpgcom  27772  colhp  27775  dfcgra2  27835  nbgrel  28351  nbgrsym  28374  wlkson  28667  isspthonpth  28760  usgr2pth0  28776  wwlksnextinj  28907  elwspths2spth  28975  rusgrnumwwlkl1  28976  clwwlknclwwlkdifnum  28987  clwwlkn1  29048  clwwlkn2  29051  iseupthf1o  29209  eupth2lem2  29226  frgrncvvdeqlem2  29307  fusgr2wsp2nb  29341  fusgreg2wsp  29343  frgrreg  29401  frgrregord013  29402  h2hcau  29984  nmopub  30913  nmfnleub  30930  chrelati  31369  cvexchlem  31373  mdsymlem8  31415  sumdmdii  31420  13an22anass  31458  2reucom  31472  reuxfrdf  31483  dmrab  31489  difrab2  31490  ressupprn  31672  2ndpreima  31689  fpwrelmapffslem  31717  xrofsup  31740  mgccnv  31929  pmtrprfv2  32009  smatrcl  32466  cnvordtrestixx  32583  issgon  32811  eulerpartlemr  33063  eulerpartlemgvv  33065  ballotlem2  33177  sgn3da  33230  oddprm2  33357  bnj257  33408  bnj545  33596  bnj594  33613  satfv0  34039  satfvsuclem1  34040  dfdm5  34433  dfrn5  34434  elima4  34436  elfix  34564  dffix2  34566  brimg  34598  brsuccf  34602  dfrecs2  34611  dfrdg4  34612  cgrcomlr  34659  ofscom  34668  btwnexch  34686  fscgr  34741  bj-df-ifc  35120  bj-dfmpoa  35662  bj-eldiag  35720  bj-imdirco  35734  bj-ccinftydisj  35757  mptsnunlem  35882  topdifinffinlem  35891  fvineqsneq  35956  wl-cases2-dnf  36044  wl-ax11-lem4  36113  fin2solem  36137  poimirlem26  36177  poimirlem30  36181  poimirlem32  36183  ftc1anclem6  36229  ftc1anc  36232  heibor1  36342  isdrngo3  36491  isdmn3  36606  anan  36757  br1cnvinxp  36789  inxpxrn  36930  prtlem70  37392  lrelat  37549  islshpat  37552  atlrelat1  37856  ishlat2  37888  cdlemb3  39142  diblsmopel  39707  dicelval3  39716  diclspsn  39730  uzindd  40507  3factsumint2  40552  3factsumint3  40553  3factsumint  40555  fz1eqin  41150  diophrex  41156  fphpd  41197  fzneg  41364  expdioph  41405  dford4  41411  lnr2i  41501  fgraphopab  41595  omge2  41691  oadif1lem  41772  oadif1  41773  ifpancor  41858  ifpidg  41885  ifpid2g  41887  ifpid1g  41888  ifpim23g  41889  rp-fakeoranass  41908  minregex  41928  dfid7  42006  dfrtrcl5  42023  relexp0eq  42095  fsovrfovd  42403  rr-grothprimbi  42697  uunT1p1  43185  uun132p1  43190  un2122  43194  uun2131p1  43196  uunT12p1  43204  uunT12p2  43205  uunT12p3  43206  uun2221  43217  uun2221p1  43218  uun2221p2  43219  3impdirp1  43220  ancomstVD  43269  icccncfext  44248  dvnmul  44304  dvmptfprodlem  44305  dvnprodlem2  44308  fourierdlem42  44510  fourierdlem83  44550  f1cof1b  45429  2reu3  45462  2reu7  45463  2reu8  45464  2reuimp0  45466  ndmaovcom  45557  an4com24  45620  4an21  45622  sprvalpwn0  45795  prpair  45813  prproropf1olem0  45814  2zrngnmrid  46368  opeliun2xp  46528  rrx2linest  46948  pm5.32dav  46999  iscnrm3lem3  47088  thincsect2  47198