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  637  bianassc  644  an12  646  an13  648  an42  658  andir  1011  cases2  1048  dfifp6  1069  ifpn  1074  4anpull2  1363  excxor  1518  cador  1610  cadcoma  1614  exancom  1863  19.42v  1955  19.42  2244  sbel2x  2479  eu6  2575  moanmo  2623  2eu3  2655  2eu7  2659  2eu8  2660  eq2tri  2799  r19.42v  3170  rexcomf  3277  rabswap  3399  spc2ed  3544  euxfr2w  3667  euxfr2  3669  rmo4  3677  reu8  3680  rmo3f  3681  reuxfrd  3695  rmo3  3828  difin2  4242  rcompleq  4246  euelss  4273  ssunsn  4772  uniprg  4867  inuni  5287  eqvinop  5435  elxp2  5648  opeliun2xp  5692  elvvv  5700  brinxp2  5702  dmuni  5863  imadmrn  6029  asymref2  6074  cnvopab  6094  cnvxp  6115  xpdifid  6126  cnvcnvsn  6177  opswap  6187  mptpreima  6196  xpco  6247  dfpo2  6254  fncnv  6565  fnres  6619  mptfnf  6627  dff1o2  6779  f13dfv  7222  fliftcnv  7259  isoini  7286  elrnmpores  7498  ndmovcom  7547  uniuni  7709  opabex3rd  7912  mptmpoopabbrd  8026  fsplit  8060  brtpos  8178  tposmpo  8206  oaord  8475  nnaord  8548  naddasslem1  8623  naddasslem2  8624  brinxper  8666  pmex  8771  mapsnend  8976  snmapen  8978  xpsnen  8992  xpcomco  8998  elfi2  9320  supmo  9358  infmo  9403  frind  9665  cp  9806  dfac5lem1  10036  dfac5lem2  10037  dfac2b  10044  kmlem3  10066  cflim3  10175  brdom7disj  10444  brdom6disj  10445  recmulnq  10878  lesub0  11658  wloglei  11673  creur  12144  indstr  12857  xmulcom  13209  xmulneg1  13212  xmulf  13215  iccneg  13416  fzrev  13532  injresinj  13737  rediv  15084  imdiv  15091  lenegsq  15274  o1lo1  15490  fsumcom2  15727  fsumcom  15728  fprodcom2  15940  fprodcom  15941  divalglem10  16362  smueqlem  16450  gcdcom  16473  lcmcom  16553  isprm2  16642  isprm7  16669  infpn2  16875  imasleval  17496  dfiso3  17731  posglbmo  18367  odulatb  18391  oduclatb  18464  oppgid  19322  gsumcom  19943  gsumcom3  19944  dfrhm2  20445  xrsdsreclb  21403  opsrtoslem1  22043  psdmvr  22145  madutpos  22617  fvmptnn04if  22824  ntreq0  23052  ist0-3  23320  txkgen  23627  trfil2  23862  flimrest  23958  blres  24406  metrest  24499  restmetu  24545  elii1  24912  isclmp  25074  evthicc2  25437  ovolfcl  25443  dyaddisj  25573  iblpos  25770  itgposval  25773  ditgsplit  25838  itgsubst  26026  sincosq3sgn  26477  cos11  26510  dvdsflsumcom  27165  fsumvma  27190  logfaclbnd  27199  dchrelbas3  27215  lgsdi  27311  lgsquadlem3  27359  2lgslem1a  27368  lestri3  27733  ltsrec  27807  istrkg2ld  28542  tgjustf  28555  tgcgr4  28613  mirreu3  28736  hpgcom  28849  colhp  28852  dfcgra2  28912  nbgrel  29423  nbgrsym  29446  wlkson  29738  dfpth2  29812  isspthonpth  29832  usgr2pth0  29848  wwlksnextinj  29982  elwspths2spth  30053  rusgrnumwwlkl1  30054  clwwlknclwwlkdifnum  30065  clwwlkn1  30126  clwwlkn2  30129  iseupthf1o  30287  eupth2lem2  30304  frgrncvvdeqlem2  30385  fusgr2wsp2nb  30419  fusgreg2wsp  30421  frgrreg  30479  frgrregord013  30480  h2hcau  31065  nmopub  31994  nmfnleub  32011  chrelati  32450  cvexchlem  32454  mdsymlem8  32496  sumdmdii  32501  13an22anass  32548  2reucom  32564  reuxfrdf  32575  dmrab  32581  difrab2  32582  ressupprn  32778  2ndpreima  32796  fpwrelmapffslem  32820  xrofsup  32855  sgn3da  32922  mgccnv  33074  pmtrprfv2  33164  smatrcl  33956  cnvordtrestixx  34073  issgon  34283  eulerpartlemr  34534  eulerpartlemgvv  34536  ballotlem2  34649  oddprm2  34815  bnj257  34866  bnj545  35053  bnj594  35070  nfan1c  35231  satfv0  35556  satfvsuclem1  35557  dfdm5  35971  dfrn5  35972  elima4  35974  elfix  36099  dffix2  36101  brimg  36133  lemsuccf  36137  dfrecs2  36148  dfrdg4  36149  cgrcomlr  36196  ofscom  36205  btwnexch  36223  fscgr  36278  bj-df-ifc  36861  bj-axseprep  37397  bj-dfmpoa  37446  bj-eldiag  37506  bj-imdirco  37520  bj-ccinftydisj  37543  mptsnunlem  37668  topdifinffinlem  37677  fvineqsneq  37742  wl-cases2-dnf  37851  fin2solem  37941  poimirlem26  37981  poimirlem30  37985  poimirlem32  37987  ftc1anclem6  38033  ftc1anc  38036  heibor1  38145  isdrngo3  38294  isdmn3  38409  anan  38570  br1cnvinxp  38594  raldmqseu  38700  inxpxrn  38753  prtlem70  39317  lrelat  39474  islshpat  39477  atlrelat1  39781  ishlat2  39813  cdlemb3  41066  diblsmopel  41631  dicelval3  41640  diclspsn  41654  uzindd  42431  3factsumint2  42475  3factsumint3  42476  3factsumint  42478  fimgmcyc  42993  eu6w  43123  fz1eqin  43215  diophrex  43221  fphpd  43262  fzneg  43428  expdioph  43469  dford4  43475  lnr2i  43562  fgraphopab  43649  omge2  43744  oadif1lem  43825  oadif1  43826  ifpancor  43909  ifpidg  43936  ifpid2g  43938  ifpid1g  43939  ifpim23g  43940  rp-fakeoranass  43959  minregex  43979  dfid7  44057  dfrtrcl5  44074  relexp0eq  44146  fsovrfovd  44454  rr-grothprimbi  44740  uunT1p1  45225  uun132p1  45230  un2122  45234  uun2131p1  45236  uunT12p1  45244  uunT12p2  45245  uunT12p3  45246  uun2221  45257  uun2221p1  45258  uun2221p2  45259  3impdirp1  45260  ancomstVD  45309  icccncfext  46333  dvnmul  46389  dvmptfprodlem  46390  dvnprodlem2  46393  fourierdlem42  46595  fourierdlem83  46635  f1cof1b  47537  2reu3  47570  2reu7  47571  2reu8  47572  2reuimp0  47574  ndmaovcom  47665  an4com24  47728  4an21  47730  sprvalpwn0  47955  prpair  47973  prproropf1olem0  47974  clnbgrel  48316  clnbgrsym  48326  2zrngnmrid  48744  rrx2linest  49230  pm5.32dav  49281  resinsnALT  49360  catcinv  49886  thincsect2  49955  lmdfval  50136  cmdfval  50137