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  excxor  1512  cador  1604  cadcoma  1608  exancom  1858  19.42v  1950  19.42  2233  sbel2x  2476  eu6  2571  moanmo  2619  2eu3  2651  2eu7  2655  2eu8  2656  eq2tri  2801  r19.42v  3188  rexcomf  3300  rabswap  3442  spc2ed  3600  euxfr2w  3728  euxfr2  3730  rmo4  3738  reu8  3741  rmo3f  3742  reuxfrd  3756  rmo3  3897  difin2  4306  rcompleq  4310  euelss  4337  ssunsn  4832  uniprg  4927  inuni  5355  eqvinop  5497  elxp2  5712  elvvv  5763  brinxp2  5765  dmuni  5927  imadmrn  6089  asymref2  6139  cnvopab  6159  cnvxp  6178  xpdifid  6189  cnvcnvsn  6240  opswap  6250  mptpreima  6259  xpco  6310  dfpo2  6317  fncnv  6640  fnres  6695  mptfnf  6703  dff1o2  6853  f13dfv  7293  fliftcnv  7330  isoini  7357  elrnmpores  7570  ndmovcom  7619  uniuni  7780  opabex3rd  7989  mptmpoopabbrd  8103  mptmpoopabbrdOLD  8104  mptmpoopabbrdOLDOLD  8106  fsplit  8140  brtpos  8258  tposmpo  8286  oaord  8583  nnaord  8655  naddasslem1  8730  naddasslem2  8731  brinxper  8772  pmex  8869  mapsnend  9074  snmapen  9076  xpsnen  9093  xpcomco  9100  elfi2  9451  supmo  9489  infmo  9532  frind  9787  cp  9928  dfac5lem1  10160  dfac5lem2  10161  dfac2b  10168  kmlem3  10190  cflim3  10299  brdom7disj  10568  brdom6disj  10569  recmulnq  11001  lesub0  11777  wloglei  11792  creur  12257  indstr  12955  xmulcom  13304  xmulneg1  13307  xmulf  13310  iccneg  13508  fzrev  13623  injresinj  13823  rediv  15166  imdiv  15173  lenegsq  15355  o1lo1  15569  fsumcom2  15806  fsumcom  15807  fprodcom2  16016  fprodcom  16017  divalglem10  16435  smueqlem  16523  gcdcom  16546  lcmcom  16626  isprm2  16715  isprm7  16741  infpn2  16946  imasleval  17587  dfiso3  17820  posglbmo  18469  odulatb  18491  oduclatb  18564  oppgid  19389  gsumcom  20009  gsumcom3  20010  dfrhm2  20490  xrsdsreclb  21448  opsrtoslem1  22096  madutpos  22663  fvmptnn04if  22870  ntreq0  23100  ist0-3  23368  txkgen  23675  trfil2  23910  flimrest  24006  blres  24456  metrest  24552  restmetu  24598  elii1  24977  isclmp  25143  evthicc2  25508  ovolfcl  25514  dyaddisj  25644  iblpos  25842  itgposval  25845  ditgsplit  25910  itgsubst  26104  sincosq3sgn  26556  cos11  26589  dvdsflsumcom  27245  fsumvma  27271  logfaclbnd  27280  dchrelbas3  27296  lgsdi  27392  lgsquadlem3  27440  2lgslem1a  27449  sletri3  27814  nocvxmin  27837  sltrec  27879  istrkg2ld  28482  tgjustf  28495  tgcgr4  28553  mirreu3  28676  hpgcom  28789  colhp  28792  dfcgra2  28852  nbgrel  29371  nbgrsym  29394  wlkson  29688  isspthonpth  29781  usgr2pth0  29797  wwlksnextinj  29928  elwspths2spth  29996  rusgrnumwwlkl1  29997  clwwlknclwwlkdifnum  30008  clwwlkn1  30069  clwwlkn2  30072  iseupthf1o  30230  eupth2lem2  30247  frgrncvvdeqlem2  30328  fusgr2wsp2nb  30362  fusgreg2wsp  30364  frgrreg  30422  frgrregord013  30423  h2hcau  31007  nmopub  31936  nmfnleub  31953  chrelati  32392  cvexchlem  32396  mdsymlem8  32438  sumdmdii  32443  13an22anass  32492  2reucom  32507  reuxfrdf  32518  dmrab  32524  difrab2  32525  ressupprn  32704  2ndpreima  32722  fpwrelmapffslem  32749  xrofsup  32777  mgccnv  32973  pmtrprfv2  33090  smatrcl  33756  cnvordtrestixx  33873  issgon  34103  eulerpartlemr  34355  eulerpartlemgvv  34357  ballotlem2  34469  sgn3da  34522  oddprm2  34648  bnj257  34699  bnj545  34887  bnj594  34904  nfan1c  35065  satfv0  35342  satfvsuclem1  35343  dfdm5  35753  dfrn5  35754  elima4  35756  elfix  35884  dffix2  35886  brimg  35918  brsuccf  35922  dfrecs2  35931  dfrdg4  35932  cgrcomlr  35979  ofscom  35988  btwnexch  36006  fscgr  36061  bj-df-ifc  36562  bj-dfmpoa  37100  bj-eldiag  37158  bj-imdirco  37172  bj-ccinftydisj  37195  mptsnunlem  37320  topdifinffinlem  37329  fvineqsneq  37394  wl-cases2-dnf  37492  wl-ax11-lem4  37568  fin2solem  37592  poimirlem26  37632  poimirlem30  37636  poimirlem32  37638  ftc1anclem6  37684  ftc1anc  37687  heibor1  37796  isdrngo3  37945  isdmn3  38060  anan  38209  br1cnvinxp  38237  inxpxrn  38376  prtlem70  38838  lrelat  38995  islshpat  38998  atlrelat1  39302  ishlat2  39334  cdlemb3  40588  diblsmopel  41153  dicelval3  41162  diclspsn  41176  uzindd  41958  3factsumint2  42003  3factsumint3  42004  3factsumint  42006  fimgmcyc  42520  eu6w  42662  fz1eqin  42756  diophrex  42762  fphpd  42803  fzneg  42970  expdioph  43011  dford4  43017  lnr2i  43104  fgraphopab  43191  omge2  43287  oadif1lem  43368  oadif1  43369  ifpancor  43453  ifpidg  43480  ifpid2g  43482  ifpid1g  43483  ifpim23g  43484  rp-fakeoranass  43503  minregex  43523  dfid7  43601  dfrtrcl5  43618  relexp0eq  43690  fsovrfovd  43998  rr-grothprimbi  44290  uunT1p1  44778  uun132p1  44783  un2122  44787  uun2131p1  44789  uunT12p1  44797  uunT12p2  44798  uunT12p3  44799  uun2221  44810  uun2221p1  44811  uun2221p2  44812  3impdirp1  44813  ancomstVD  44862  icccncfext  45842  dvnmul  45898  dvmptfprodlem  45899  dvnprodlem2  45902  fourierdlem42  46104  fourierdlem83  46144  f1cof1b  47026  2reu3  47059  2reu7  47060  2reu8  47061  2reuimp0  47063  ndmaovcom  47154  an4com24  47217  4an21  47219  sprvalpwn0  47407  prpair  47425  prproropf1olem0  47426  clnbgrel  47752  clnbgrsym  47761  2zrngnmrid  48099  opeliun2xp  48177  rrx2linest  48591  pm5.32dav  48642  iscnrm3lem3  48731  thincsect2  48858