Theorem ancom 466

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 465	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜓 ∧ 𝜑))
2		pm3.22 465	. 2 ⊢ ((𝜓 ∧ 𝜑) → (𝜑 ∧ 𝜓))
3	1, 2	impbii 212	1 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜓 ∧ 𝜑))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  ancomd  467  biancomi  468  biancomd  469  ancomst  470  pm4.71r  568  pm5.32ri  586  pm5.32rd  589  an2anr  648  bianassc  656  an12  658  an13  660  an42  670  andir  1026  cases2  1063  dfifp6  1084  ifpn  1090  13an22anass  1379  4anpull2OLD  1383  excxor  1546  cador  1641  cadcoma  1645  exancom  1894  19.42v  1986  19.42  2275  sbel2x  2508  eu6  2604  moanmo  2652  2eu3  2683  2eu7  2687  2eu8  2688  eq2tri  2827  r19.42v  3199  rexcomf  3306  rabswap  3427  spc2ed  3562  euxfr2w  3685  euxfr2  3687  rmo4  3695  reu8  3698  rmo3f  3699  reuxfrd  3713  rmo3  3843  difin2  4254  rcompleq  4258  euelss  4285  ssunsn  4796  uniprg  4890  inuni  5322  eqvinop  5471  elxp2  5687  opeliun2xp  5731  elvvv  5739  brinxp2  5741  dmuni  5906  imadmrn  6074  asymref2  6119  cnvopab  6139  cnvxp  6156  xpdifid  6167  xpdifcnvepel  6168  cnvcnvsn  6222  opswap  6232  mptpreima  6241  xpco  6294  dfpo2  6301  fncnv  6613  fnres  6666  mptfnf  6674  dff1o2  6830  f13dfv  7278  fliftcnv  7315  isoini  7342  elrnmpores  7554  ndmovcom  7603  uniuni  7763  opabex3rd  7965  mptmpoopabbrd  8080  fsplit  8114  brtpos  8233  tposmpo  8261  oaord  8534  nnaord  8607  naddasslem1  8683  naddasslem2  8684  brinxper  8726  pmex  8831  mapsnend  9036  snmapen  9038  xpsnen  9052  xpcomco  9058  elfi2  9377  supmo  9415  infmo  9460  frind  9725  cp  9886  dfac5lem1  10119  dfac5lem2  10120  dfac2b  10126  kmlem3  10148  cflim3  10257  brdom7disj  10526  brdom6disj  10527  recmulnq  10960  lesub0  11742  wloglei  11757  creur  12223  indstr  12952  xmulcom  13304  xmulneg1  13307  xmulf  13310  iccneg  13511  fzrev  13628  injresinj  13833  sgn3da  15158  rediv  15202  imdiv  15209  lenegsq  15392  o1lo1  15608  fsumcom2  15844  fsumcom  15845  fprodcom2  16057  fprodcom  16058  divalglem10  16478  smueqlem  16566  gcdcom  16589  lcmcom  16669  isprm2  16758  isprm7  16785  infpn2  16991  imasleval  17613  dfiso3  17848  posglbmo  18484  odulatb  18508  oduclatb  18581  oppgid  19450  gsumcom  20071  gsumcom3  20072  dfrhm2  20582  isdrng5  20884  isfieldidl  21416  xrsdsreclb  21594  opsrtoslem1  22236  psdmvr  22362  madutpos  22829  fvmptnn04if  23036  ntreq0  23264  ist0-3  23532  txkgen  23840  trfil2  24075  flimrest  24171  blres  24619  metrest  24712  restmetu  24758  elii1  25125  isclmp  25287  evthicc2  25650  ovolfcl  25656  dyaddisj  25786  iblpos  25983  itgposval  25986  ditgsplit  26051  itgsubst  26239  sincosq3sgn  26696  cos11  26729  dvdsflsumcom  27383  fsumvma  27408  logfaclbnd  27417  dchrelbas3  27433  lgsdi  27529  lgsquadlem3  27577  2lgslem1a  27586  lestri3  27950  ltsrec  28025  istrkg2ld  28760  tgjustf  28773  tgcgr4  28831  mirreu3  28962  hpgcom  29080  colhp  29083  dfcgra2  29172  prlngsym  29222  dfprlng2  29228  nbgrel  29724  nbgrsym  29747  wlkson  30038  dfpth2  30117  isspthonpth  30138  usgr2pth0  30154  wwlksnextinj  30291  elwspths2spth  30362  rusgrnumwwlkl1  30363  clwwlknclwwlkdifnum  30374  clwwlkn1  30435  clwwlkn2  30438  iseupthf1o  30600  eupth2lem2  30617  frgrncvvdeqlem2  30698  fusgr2wsp2nb  30732  fusgreg2wsp  30734  frgrreg  30792  frgrregord013  30793  h2hcau  31378  nmopub  32307  nmfnleub  32324  chrelati  32763  cvexchlem  32767  mdsymlem8  32809  sumdmdii  32814  2reucom  32873  reuxfrdf  32884  dmrab  32890  difrab2  32891  ififcom  32943  ressupprn  33082  2ndpreima  33100  fpwrelmapffslem  33123  xrofsup  33158  mgccnv  33359  pmtrprfv2  33448  smatrcl  34226  cnvordtrestixx  34343  issgon  34553  eulerpartlemr  34805  eulerpartlemgvv  34807  ballotlem2  34920  oddprm2  35083  bnj257  35137  bnj545  35324  bnj594  35341  nfan1c  35502  satfv0  35863  satfvsuclem1  35864  dfdm5  36278  dfrn5  36279  elima4  36281  elfix  36406  dffix2  36408  brimg  36440  lemsuccf  36444  dfrecs2  36455  dfrdg4  36456  cgrcomlr  36503  ofscom  36512  btwnexch  36530  fscgr  36585  bj-df-ifc  37206  bj-axseprep  37744  bj-dfmpoa  37793  bj-eldiag  37853  bj-imdirco  37867  bj-ccinftydisj  37890  mptsnunlem  38017  topdifinffinlem  38026  fvineqsneq  38091  wl-cases2-dnf  38200  fin2solem  38290  poimirlem26  38330  poimirlem30  38334  poimirlem32  38336  ftc1anclem6  38382  ftc1anc  38385  heibor1  38494  isdrngo3  38643  isdmn3  38758  anan  38917  br1cnvinxp  38941  raldmqseu  39047  inxpxrn  39100  prtlem70  39664  lrelat  39821  islshpat  39824  atlrelat1  40128  ishlat2  40160  cdlemb3  41413  diblsmopel  41978  dicelval3  41987  diclspsn  42001  uzindd  42778  3factsumint2  42822  3factsumint3  42823  3factsumint  42825  fimgmcyc  43335  eu6w  43441  fz1eqin  43533  diophrex  43539  fphpd  43576  fzneg  43742  expdioph  43783  dford4  43789  lnr2i  43876  fgraphopab  43963  omge2  44058  oadif1lem  44139  oadif1  44140  ifpancor  44223  ifpidg  44250  ifpid2g  44252  ifpid1g  44253  ifpim23g  44254  rp-fakeoranass  44273  minregex  44293  dfid7  44371  dfrtrcl5  44388  relexp0eq  44460  fsovrfovd  44768  rr-grothprimbi  45038  uunT1p1  45522  uun132p1  45527  un2122  45531  uun2131p1  45533  uunT12p1  45541  uunT12p2  45542  uunT12p3  45543  uun2221  45554  uun2221p1  45555  uun2221p2  45556  3impdirp1  45557  ancomstVD  45606  icccncfext  46634  dvnmul  46690  dvmptfprodlem  46691  dvnprodlem2  46694  fourierdlem42  46896  fourierdlem83  46936  f1cof1b  47847  2reu3  47880  2reu7  47881  2reu8  47882  2reuimp0  47884  ndmaovcom  47975  an4com24  48038  4an21  48040  sprvalpwn0  48265  prpair  48283  prproropf1olem0  48284  clnbgrel  48626  clnbgrsym  48636  2zrngnmrid  49054  isidom3  49143  rrx2linest  49555  pm5.32dav  49605  resinsnALT  49684  catcinv  50210  thincsect2  50279  lmdfval  50460  cmdfval  50461  2alsraln0  50628