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  2273  sbel2x  2504  eu6  2600  moanmo  2648  2eu3  2679  2eu7  2683  2eu8  2684  eq2tri  2823  r19.42v  3195  rexcomf  3302  rabswap  3422  spc2ed  3556  euxfr2w  3678  euxfr2  3680  rmo4  3688  reu8  3691  rmo3f  3692  reuxfrd  3706  rmo3  3836  difin2  4247  rcompleq  4251  euelss  4278  ssunsn  4789  uniprg  4883  inuni  5311  eqvinop  5456  eqvinot  5457  elxp2  5675  opeliun2xp  5719  elvvv  5727  brinxp2  5729  dmuni  5896  imadmrnOLD  6068  asymref2  6111  cnvopab  6131  cnvxp  6147  cnvxpOLD  6148  xpdifid  6159  xpdifcnvepel  6160  cnvcnvsn  6219  opswap  6229  mptpreima  6238  xpco  6291  dfpo2  6298  fncnv  6611  fnres  6664  mptfnf  6672  dff1o2  6828  f13dfv  7280  fliftcnv  7317  isoini  7344  elrnmpores  7556  ndmovcom  7606  uniuni  7774  opabex3rd  7976  mptmpoopabbrd  8092  fsplit  8126  brtpos  8245  tposmpo  8273  oaord  8548  nnaord  8621  naddasslem1  8697  naddasslem2  8698  brinxper  8740  pmex  8845  mapsnend  9057  snmapen  9059  xpsnen  9073  xpcomco  9079  elfi2  9399  supmo  9437  infmo  9482  frind  9747  cp  9947  dfac5lem1  10195  dfac5lem2  10196  dfac2b  10202  kmlem3  10224  cflim3  10333  brdom7disj  10603  brdom6disj  10604  recmulnq  11042  lesub0  11826  wloglei  11841  creur  12307  indstr  13036  xmulcom  13389  xmulneg1  13392  xmulf  13395  iccneg  13596  fzrev  13714  injresinj  13919  sgn3da  15247  rediv  15291  imdiv  15298  lenegsq  15481  o1lo1  15697  fsumcom2  15933  fsumcom  15934  fprodcom2  16144  fprodcom  16145  divalglem10  16565  smueqlem  16653  gcdcom  16678  lcmcom  16761  isprm2  16850  isprm7  16877  infpn2  17084  imasleval  17706  dfiso3  17941  posglbmo  18577  odulatb  18601  oduclatb  18674  oppgid  19563  gsumcom  20184  gsumcom3  20185  dfring3  20511  dfrhm2  20697  isdrng5  21001  isfieldidl  21533  xrsdsreclb  21713  opsrtoslem1  22357  psdmvr  22483  madutpos  22950  fvmptnn04if  23160  ntreq0  23388  ist0-3  23656  txkgen  23964  trfil2  24199  flimrest  24295  blres  24743  metrest  24836  restmetu  24882  elii1  25249  isclmp  25411  evthicc2  25774  ovolfcl  25780  dyaddisj  25910  iblpos  26106  itgposval  26109  ditgsplit  26174  itgsubst  26362  sincosq3sgn  26822  cos11  26854  dvdsflsumcom  27508  fsumvma  27533  logfaclbnd  27542  dchrelbas3  27558  lgsdi  27654  lgsquadlem3  27702  2lgslem1a  27711  lestri3  28105  ltsrec  28180  istrkg2ld  28915  tgjustf  28928  tgcgr4  28987  mirreu3  29119  hpgcom  29238  colhp  29241  dfcgra2  29331  prlngsym  29412  dfprlng2  29418  nbgrel  29914  nbgrsym  29937  wlkson  30228  dfpth2  30307  isspthonpth  30328  usgr2pth0  30344  wwlksnextinj  30481  elwspths2spth  30552  rusgrnumwwlkl1  30553  clwwlknclwwlkdifnum  30564  clwwlkn1  30625  clwwlkn2  30628  iseupthf1o  30796  eupth2lem2  30813  frgrncvvdeqlem2  30894  fusgr2wsp2nb  30928  fusgreg2wsp  30930  frgrreg  30988  frgrregord013  30989  h2hcau  31574  nmopub  32503  nmfnleub  32520  chrelati  32959  cvexchlem  32963  mdsymlem8  33005  sumdmdii  33010  2reucom  33069  reuxfrdf  33080  dmrab  33086  difrab2  33087  ififcom  33139  ressupprn  33276  2ndpreima  33294  fpwrelmapffslem  33317  xrofsup  33352  mgccnv  33553  pmtrprfv2  33642  smatrcl  34421  cnvordtrestixx  34538  issgon  34748  eulerpartlemr  34999  eulerpartlemgvv  35001  ballotlem2  35114  oddprm2  35277  bnj257  35331  bnj545  35518  bnj594  35535  nfan1c  35696  satfv0  36102  satfvsuclem1  36103  dfdm5  36517  dfrn5  36518  elima4  36520  elfix  36645  dffix2  36647  brimg  36679  lemsuccf  36683  dfrecs2  36694  dfrdg4  36695  cgrcomlr  36743  ofscom  36752  btwnexch  36770  fscgr  36825  bj-df-ifc  37430  bj-axseprep  37970  bj-dfmpoa  38019  bj-eldiag  38077  bj-imdirco  38091  bj-ccinftydisj  38114  mptsnunlem  38241  topdifinffinlem  38250  fvineqsneq  38315  wl-cases2-dnf  38424  fin2solem  38509  poimirlem26  38544  poimirlem30  38548  poimirlem32  38550  ftc1anclem6  38596  ftc1anc  38599  heibor1  38724  isdrngo3  38873  isdmn3  38988  anan  39147  br1cnvinxp  39171  raldmqseu  39277  inxpxrn  39330  prtlem70  39894  lrelat  40051  islshpat  40054  atlrelat1  40358  ishlat2  40390  cdlemb3  41643  diblsmopel  42208  dicelval3  42217  diclspsn  42231  uzindd  43008  3factsumint2  43052  3factsumint3  43053  3factsumint  43055  fimgmcyc  43578  eu6w  43667  fz1eqin  43759  diophrex  43765  fphpd  43802  fzneg  43968  expdioph  44009  dford4  44015  lnr2i  44102  fgraphopab  44189  omge2  44284  oadif1lem  44365  oadif1  44366  ifpancor  44449  ifpidg  44476  ifpid2g  44478  ifpid1g  44479  ifpim23g  44480  rp-fakeoranass  44499  minregex  44519  dfid7  44597  dfrtrcl5  44614  relexp0eq  44686  fsovrfovd  44994  rr-grothprimbi  45264  uunT1p1  45748  uun132p1  45753  un2122  45757  uun2131p1  45759  uunT12p1  45767  uunT12p2  45768  uunT12p3  45769  uun2221  45780  uun2221p1  45781  uun2221p2  45782  3impdirp1  45783  ancomstVD  45832  icccncfext  46866  dvnmul  46922  dvmptfprodlem  46923  dvnprodlem2  46926  fourierdlem42  47128  fourierdlem83  47168  f1cof1b  48116  2reu3  48149  2reu7  48150  2reu8  48151  2reuimp0  48153  ndmaovcom  48244  an4com24  48307  4an21  48309  sprvalpwn0  48534  prpair  48552  prproropf1olem0  48553  clnbgrel  48895  clnbgrsym  48905  2zrngnmrid  49322  isidom3  49411  rrx2linest  49823  pm5.32rda  49873  resinsnALT  49950  catcinv  50476  thincsect2  50545  lmdfval  50726  cmdfval  50727  2alsraln0  50882