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  2272  sbel2x  2503  eu6  2599  moanmo  2647  2eu3  2678  2eu7  2682  2eu8  2683  eq2tri  2822  r19.42v  3194  rexcomf  3301  rabswap  3421  spc2ed  3555  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  5314  eqvinop  5463  elxp2  5679  opeliun2xp  5723  elvvv  5731  brinxp2  5733  dmuni  5898  imadmrn  6066  asymref2  6111  cnvopab  6131  cnvxp  6148  cnvxpOLD  6149  xpdifid  6160  xpdifcnvepel  6161  cnvcnvsn  6215  opswap  6225  mptpreima  6234  xpco  6287  dfpo2  6294  fncnv  6606  fnres  6659  mptfnf  6667  dff1o2  6823  f13dfv  7275  fliftcnv  7312  isoini  7339  elrnmpores  7551  ndmovcom  7601  uniuni  7761  opabex3rd  7963  mptmpoopabbrd  8080  fsplit  8114  brtpos  8233  tposmpo  8261  oaord  8534  nnaord  8607  naddasslem1  8683  naddasslem2  8684  brinxper  8726  pmex  8831  mapsnend  9043  snmapen  9045  xpsnen  9059  xpcomco  9065  elfi2  9384  supmo  9422  infmo  9467  frind  9732  cp  9893  dfac5lem1  10126  dfac5lem2  10127  dfac2b  10133  kmlem3  10155  cflim3  10264  brdom7disj  10534  brdom6disj  10535  recmulnq  10973  lesub0  11755  wloglei  11770  creur  12236  indstr  12965  xmulcom  13318  xmulneg1  13321  xmulf  13324  iccneg  13525  fzrev  13642  injresinj  13847  sgn3da  15174  rediv  15218  imdiv  15225  lenegsq  15408  o1lo1  15624  fsumcom2  15860  fsumcom  15861  fprodcom2  16071  fprodcom  16072  divalglem10  16492  smueqlem  16580  gcdcom  16603  lcmcom  16683  isprm2  16772  isprm7  16799  infpn2  17005  imasleval  17627  dfiso3  17862  posglbmo  18498  odulatb  18522  oduclatb  18595  oppgid  19483  gsumcom  20104  gsumcom3  20105  dfrhm2  20615  isdrng5  20917  isfieldidl  21449  xrsdsreclb  21627  opsrtoslem1  22271  psdmvr  22397  madutpos  22864  fvmptnn04if  23074  ntreq0  23302  ist0-3  23570  txkgen  23878  trfil2  24113  flimrest  24209  blres  24657  metrest  24750  restmetu  24796  elii1  25163  isclmp  25325  evthicc2  25688  ovolfcl  25694  dyaddisj  25824  iblpos  26020  itgposval  26023  ditgsplit  26088  itgsubst  26276  sincosq3sgn  26738  cos11  26770  dvdsflsumcom  27424  fsumvma  27449  logfaclbnd  27458  dchrelbas3  27474  lgsdi  27570  lgsquadlem3  27618  2lgslem1a  27627  lestri3  27991  ltsrec  28066  istrkg2ld  28801  tgjustf  28814  tgcgr4  28873  mirreu3  29005  hpgcom  29124  colhp  29127  dfcgra2  29217  prlngsym  29298  dfprlng2  29304  nbgrel  29800  nbgrsym  29823  wlkson  30114  dfpth2  30193  isspthonpth  30214  usgr2pth0  30230  wwlksnextinj  30367  elwspths2spth  30438  rusgrnumwwlkl1  30439  clwwlknclwwlkdifnum  30450  clwwlkn1  30511  clwwlkn2  30514  iseupthf1o  30682  eupth2lem2  30699  frgrncvvdeqlem2  30780  fusgr2wsp2nb  30814  fusgreg2wsp  30816  frgrreg  30874  frgrregord013  30875  h2hcau  31460  nmopub  32389  nmfnleub  32406  chrelati  32845  cvexchlem  32849  mdsymlem8  32891  sumdmdii  32896  2reucom  32955  reuxfrdf  32966  dmrab  32972  difrab2  32973  ififcom  33025  ressupprn  33162  2ndpreima  33180  fpwrelmapffslem  33203  xrofsup  33238  mgccnv  33439  pmtrprfv2  33528  smatrcl  34306  cnvordtrestixx  34423  issgon  34633  eulerpartlemr  34885  eulerpartlemgvv  34887  ballotlem2  35000  oddprm2  35163  bnj257  35217  bnj545  35404  bnj594  35421  nfan1c  35582  satfv0  35937  satfvsuclem1  35938  dfdm5  36352  dfrn5  36353  elima4  36355  elfix  36480  dffix2  36482  brimg  36514  lemsuccf  36518  dfrecs2  36529  dfrdg4  36530  cgrcomlr  36578  ofscom  36587  btwnexch  36605  fscgr  36660  bj-df-ifc  37281  bj-axseprep  37819  bj-dfmpoa  37868  bj-eldiag  37928  bj-imdirco  37942  bj-ccinftydisj  37965  mptsnunlem  38092  topdifinffinlem  38101  fvineqsneq  38166  wl-cases2-dnf  38275  fin2solem  38360  poimirlem26  38395  poimirlem30  38399  poimirlem32  38401  ftc1anclem6  38447  ftc1anc  38450  heibor1  38560  isdrngo3  38709  isdmn3  38824  anan  38983  br1cnvinxp  39007  raldmqseu  39113  inxpxrn  39166  prtlem70  39730  lrelat  39887  islshpat  39890  atlrelat1  40194  ishlat2  40226  cdlemb3  41479  diblsmopel  42044  dicelval3  42053  diclspsn  42067  uzindd  42844  3factsumint2  42888  3factsumint3  42889  3factsumint  42891  fimgmcyc  43416  eu6w  43522  fz1eqin  43614  diophrex  43620  fphpd  43657  fzneg  43823  expdioph  43864  dford4  43870  lnr2i  43957  fgraphopab  44044  omge2  44139  oadif1lem  44220  oadif1  44221  ifpancor  44304  ifpidg  44331  ifpid2g  44333  ifpid1g  44334  ifpim23g  44335  rp-fakeoranass  44354  minregex  44374  dfid7  44452  dfrtrcl5  44469  relexp0eq  44541  fsovrfovd  44849  rr-grothprimbi  45119  uunT1p1  45603  uun132p1  45608  un2122  45612  uun2131p1  45614  uunT12p1  45622  uunT12p2  45623  uunT12p3  45624  uun2221  45635  uun2221p1  45636  uun2221p2  45637  3impdirp1  45638  ancomstVD  45687  icccncfext  46715  dvnmul  46771  dvmptfprodlem  46772  dvnprodlem2  46775  fourierdlem42  46977  fourierdlem83  47017  f1cof1b  47965  2reu3  47998  2reu7  47999  2reu8  48000  2reuimp0  48002  ndmaovcom  48093  an4com24  48156  4an21  48158  sprvalpwn0  48383  prpair  48401  prproropf1olem0  48402  clnbgrel  48744  clnbgrsym  48754  2zrngnmrid  49171  isidom3  49260  rrx2linest  49672  pm5.32dav  49722  resinsnALT  49799  catcinv  50325  thincsect2  50394  lmdfval  50575  cmdfval  50576  2alsraln0  50746