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  2473  eu6  2568  moanmo  2616  2eu3  2648  2eu7  2652  2eu8  2653  eq2tri  2792  r19.42v  3170  rexcomf  3279  rabswap  3418  spc2ed  3570  euxfr2w  3694  euxfr2  3696  rmo4  3704  reu8  3707  rmo3f  3708  reuxfrd  3722  rmo3  3855  difin2  4267  rcompleq  4271  euelss  4298  ssunsn  4795  uniprg  4890  inuni  5308  eqvinop  5450  elxp2  5665  opeliun2xp  5709  elvvv  5717  brinxp2  5719  dmuni  5881  imadmrn  6044  asymref2  6093  cnvopab  6113  cnvxp  6133  xpdifid  6144  cnvcnvsn  6195  opswap  6205  mptpreima  6214  xpco  6265  dfpo2  6272  fncnv  6592  fnres  6648  mptfnf  6656  dff1o2  6808  f13dfv  7252  fliftcnv  7289  isoini  7316  elrnmpores  7530  ndmovcom  7579  uniuni  7741  opabex3rd  7948  mptmpoopabbrd  8062  mptmpoopabbrdOLD  8063  mptmpoopabbrdOLDOLD  8065  fsplit  8099  brtpos  8217  tposmpo  8245  oaord  8514  nnaord  8586  naddasslem1  8661  naddasslem2  8662  brinxper  8703  pmex  8807  mapsnend  9010  snmapen  9012  xpsnen  9029  xpcomco  9036  elfi2  9372  supmo  9410  infmo  9455  frind  9710  cp  9851  dfac5lem1  10083  dfac5lem2  10084  dfac2b  10091  kmlem3  10113  cflim3  10222  brdom7disj  10491  brdom6disj  10492  recmulnq  10924  lesub0  11702  wloglei  11717  creur  12187  indstr  12882  xmulcom  13233  xmulneg1  13236  xmulf  13239  iccneg  13440  fzrev  13555  injresinj  13756  rediv  15104  imdiv  15111  lenegsq  15294  o1lo1  15510  fsumcom2  15747  fsumcom  15748  fprodcom2  15957  fprodcom  15958  divalglem10  16379  smueqlem  16467  gcdcom  16490  lcmcom  16570  isprm2  16659  isprm7  16685  infpn2  16891  imasleval  17511  dfiso3  17742  posglbmo  18378  odulatb  18400  oduclatb  18473  oppgid  19295  gsumcom  19914  gsumcom3  19915  dfrhm2  20390  xrsdsreclb  21337  opsrtoslem1  21969  psdmvr  22063  madutpos  22536  fvmptnn04if  22743  ntreq0  22971  ist0-3  23239  txkgen  23546  trfil2  23781  flimrest  23877  blres  24326  metrest  24419  restmetu  24465  elii1  24838  isclmp  25004  evthicc2  25368  ovolfcl  25374  dyaddisj  25504  iblpos  25701  itgposval  25704  ditgsplit  25769  itgsubst  25963  sincosq3sgn  26416  cos11  26449  dvdsflsumcom  27105  fsumvma  27131  logfaclbnd  27140  dchrelbas3  27156  lgsdi  27252  lgsquadlem3  27300  2lgslem1a  27309  sletri3  27674  nocvxmin  27697  sltrec  27739  istrkg2ld  28394  tgjustf  28407  tgcgr4  28465  mirreu3  28588  hpgcom  28701  colhp  28704  dfcgra2  28764  nbgrel  29274  nbgrsym  29297  wlkson  29591  dfpth2  29666  isspthonpth  29686  usgr2pth0  29702  wwlksnextinj  29836  elwspths2spth  29904  rusgrnumwwlkl1  29905  clwwlknclwwlkdifnum  29916  clwwlkn1  29977  clwwlkn2  29980  iseupthf1o  30138  eupth2lem2  30155  frgrncvvdeqlem2  30236  fusgr2wsp2nb  30270  fusgreg2wsp  30272  frgrreg  30330  frgrregord013  30331  h2hcau  30915  nmopub  31844  nmfnleub  31861  chrelati  32300  cvexchlem  32304  mdsymlem8  32346  sumdmdii  32351  13an22anass  32400  2reucom  32416  reuxfrdf  32427  dmrab  32433  difrab2  32434  ressupprn  32620  2ndpreima  32638  fpwrelmapffslem  32662  xrofsup  32697  sgn3da  32766  mgccnv  32932  pmtrprfv2  33052  smatrcl  33793  cnvordtrestixx  33910  issgon  34120  eulerpartlemr  34372  eulerpartlemgvv  34374  ballotlem2  34487  oddprm2  34653  bnj257  34704  bnj545  34892  bnj594  34909  nfan1c  35070  satfv0  35352  satfvsuclem1  35353  dfdm5  35767  dfrn5  35768  elima4  35770  elfix  35898  dffix2  35900  brimg  35932  brsuccf  35936  dfrecs2  35945  dfrdg4  35946  cgrcomlr  35993  ofscom  36002  btwnexch  36020  fscgr  36075  bj-df-ifc  36575  bj-dfmpoa  37113  bj-eldiag  37171  bj-imdirco  37185  bj-ccinftydisj  37208  mptsnunlem  37333  topdifinffinlem  37342  fvineqsneq  37407  wl-cases2-dnf  37507  wl-ax11-lem4  37583  fin2solem  37607  poimirlem26  37647  poimirlem30  37651  poimirlem32  37653  ftc1anclem6  37699  ftc1anc  37702  heibor1  37811  isdrngo3  37960  isdmn3  38075  anan  38224  br1cnvinxp  38252  inxpxrn  38388  prtlem70  38857  lrelat  39014  islshpat  39017  atlrelat1  39321  ishlat2  39353  cdlemb3  40607  diblsmopel  41172  dicelval3  41181  diclspsn  41195  uzindd  41972  3factsumint2  42017  3factsumint3  42018  3factsumint  42020  fimgmcyc  42529  eu6w  42671  fz1eqin  42764  diophrex  42770  fphpd  42811  fzneg  42978  expdioph  43019  dford4  43025  lnr2i  43112  fgraphopab  43199  omge2  43294  oadif1lem  43375  oadif1  43376  ifpancor  43460  ifpidg  43487  ifpid2g  43489  ifpid1g  43490  ifpim23g  43491  rp-fakeoranass  43510  minregex  43530  dfid7  43608  dfrtrcl5  43625  relexp0eq  43697  fsovrfovd  44005  rr-grothprimbi  44291  uunT1p1  44777  uun132p1  44782  un2122  44786  uun2131p1  44788  uunT12p1  44796  uunT12p2  44797  uunT12p3  44798  uun2221  44809  uun2221p1  44810  uun2221p2  44811  3impdirp1  44812  ancomstVD  44861  icccncfext  45892  dvnmul  45948  dvmptfprodlem  45949  dvnprodlem2  45952  fourierdlem42  46154  fourierdlem83  46194  f1cof1b  47082  2reu3  47115  2reu7  47116  2reu8  47117  2reuimp0  47119  ndmaovcom  47210  an4com24  47273  4an21  47275  sprvalpwn0  47488  prpair  47506  prproropf1olem0  47507  clnbgrel  47833  clnbgrsym  47842  2zrngnmrid  48248  rrx2linest  48735  pm5.32dav  48786  resinsnALT  48865  catcinv  49392  thincsect2  49461  lmdfval  49642  cmdfval  49643