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  1011  cases2  1048  dfifp6  1069  ifpn  1074  4anpull2  1362  excxor  1516  cador  1608  cadcoma  1612  exancom  1861  19.42v  1953  19.42  2236  sbel2x  2479  eu6  2574  moanmo  2622  2eu3  2654  2eu7  2658  2eu8  2659  eq2tri  2804  r19.42v  3191  rexcomf  3303  rabswap  3446  spc2ed  3601  euxfr2w  3726  euxfr2  3728  rmo4  3736  reu8  3739  rmo3f  3740  reuxfrd  3754  rmo3  3889  difin2  4301  rcompleq  4305  euelss  4332  ssunsn  4828  uniprg  4923  inuni  5350  eqvinop  5492  elxp2  5709  opeliun2xp  5753  elvvv  5761  brinxp2  5763  dmuni  5925  imadmrn  6088  asymref2  6137  cnvopab  6157  cnvxp  6177  xpdifid  6188  cnvcnvsn  6239  opswap  6249  mptpreima  6258  xpco  6309  dfpo2  6316  fncnv  6639  fnres  6695  mptfnf  6703  dff1o2  6853  f13dfv  7294  fliftcnv  7331  isoini  7358  elrnmpores  7571  ndmovcom  7620  uniuni  7782  opabex3rd  7991  mptmpoopabbrd  8105  mptmpoopabbrdOLD  8106  mptmpoopabbrdOLDOLD  8108  fsplit  8142  brtpos  8260  tposmpo  8288  oaord  8585  nnaord  8657  naddasslem1  8732  naddasslem2  8733  brinxper  8774  pmex  8871  mapsnend  9076  snmapen  9078  xpsnen  9095  xpcomco  9102  elfi2  9454  supmo  9492  infmo  9535  frind  9790  cp  9931  dfac5lem1  10163  dfac5lem2  10164  dfac2b  10171  kmlem3  10193  cflim3  10302  brdom7disj  10571  brdom6disj  10572  recmulnq  11004  lesub0  11780  wloglei  11795  creur  12260  indstr  12958  xmulcom  13308  xmulneg1  13311  xmulf  13314  iccneg  13512  fzrev  13627  injresinj  13827  rediv  15170  imdiv  15177  lenegsq  15359  o1lo1  15573  fsumcom2  15810  fsumcom  15811  fprodcom2  16020  fprodcom  16021  divalglem10  16439  smueqlem  16527  gcdcom  16550  lcmcom  16630  isprm2  16719  isprm7  16745  infpn2  16951  imasleval  17586  dfiso3  17817  posglbmo  18457  odulatb  18479  oduclatb  18552  oppgid  19375  gsumcom  19995  gsumcom3  19996  dfrhm2  20474  xrsdsreclb  21431  opsrtoslem1  22079  psdmvr  22173  madutpos  22648  fvmptnn04if  22855  ntreq0  23085  ist0-3  23353  txkgen  23660  trfil2  23895  flimrest  23991  blres  24441  metrest  24537  restmetu  24583  elii1  24964  isclmp  25130  evthicc2  25495  ovolfcl  25501  dyaddisj  25631  iblpos  25828  itgposval  25831  ditgsplit  25896  itgsubst  26090  sincosq3sgn  26542  cos11  26575  dvdsflsumcom  27231  fsumvma  27257  logfaclbnd  27266  dchrelbas3  27282  lgsdi  27378  lgsquadlem3  27426  2lgslem1a  27435  sletri3  27800  nocvxmin  27823  sltrec  27865  istrkg2ld  28468  tgjustf  28481  tgcgr4  28539  mirreu3  28662  hpgcom  28775  colhp  28778  dfcgra2  28838  nbgrel  29357  nbgrsym  29380  wlkson  29674  dfpth2  29749  isspthonpth  29769  usgr2pth0  29785  wwlksnextinj  29919  elwspths2spth  29987  rusgrnumwwlkl1  29988  clwwlknclwwlkdifnum  29999  clwwlkn1  30060  clwwlkn2  30063  iseupthf1o  30221  eupth2lem2  30238  frgrncvvdeqlem2  30319  fusgr2wsp2nb  30353  fusgreg2wsp  30355  frgrreg  30413  frgrregord013  30414  h2hcau  30998  nmopub  31927  nmfnleub  31944  chrelati  32383  cvexchlem  32387  mdsymlem8  32429  sumdmdii  32434  13an22anass  32483  2reucom  32499  reuxfrdf  32510  dmrab  32516  difrab2  32517  ressupprn  32699  2ndpreima  32717  fpwrelmapffslem  32743  xrofsup  32771  mgccnv  32989  pmtrprfv2  33108  smatrcl  33795  cnvordtrestixx  33912  issgon  34124  eulerpartlemr  34376  eulerpartlemgvv  34378  ballotlem2  34491  sgn3da  34544  oddprm2  34670  bnj257  34721  bnj545  34909  bnj594  34926  nfan1c  35087  satfv0  35363  satfvsuclem1  35364  dfdm5  35773  dfrn5  35774  elima4  35776  elfix  35904  dffix2  35906  brimg  35938  brsuccf  35942  dfrecs2  35951  dfrdg4  35952  cgrcomlr  35999  ofscom  36008  btwnexch  36026  fscgr  36081  bj-df-ifc  36581  bj-dfmpoa  37119  bj-eldiag  37177  bj-imdirco  37191  bj-ccinftydisj  37214  mptsnunlem  37339  topdifinffinlem  37348  fvineqsneq  37413  wl-cases2-dnf  37513  wl-ax11-lem4  37589  fin2solem  37613  poimirlem26  37653  poimirlem30  37657  poimirlem32  37659  ftc1anclem6  37705  ftc1anc  37708  heibor1  37817  isdrngo3  37966  isdmn3  38081  anan  38230  br1cnvinxp  38257  inxpxrn  38396  prtlem70  38858  lrelat  39015  islshpat  39018  atlrelat1  39322  ishlat2  39354  cdlemb3  40608  diblsmopel  41173  dicelval3  41182  diclspsn  41196  uzindd  41978  3factsumint2  42023  3factsumint3  42024  3factsumint  42026  fimgmcyc  42544  eu6w  42686  fz1eqin  42780  diophrex  42786  fphpd  42827  fzneg  42994  expdioph  43035  dford4  43041  lnr2i  43128  fgraphopab  43215  omge2  43311  oadif1lem  43392  oadif1  43393  ifpancor  43477  ifpidg  43504  ifpid2g  43506  ifpid1g  43507  ifpim23g  43508  rp-fakeoranass  43527  minregex  43547  dfid7  43625  dfrtrcl5  43642  relexp0eq  43714  fsovrfovd  44022  rr-grothprimbi  44314  uunT1p1  44801  uun132p1  44806  un2122  44810  uun2131p1  44812  uunT12p1  44820  uunT12p2  44821  uunT12p3  44822  uun2221  44833  uun2221p1  44834  uun2221p2  44835  3impdirp1  44836  ancomstVD  44885  icccncfext  45902  dvnmul  45958  dvmptfprodlem  45959  dvnprodlem2  45962  fourierdlem42  46164  fourierdlem83  46204  f1cof1b  47089  2reu3  47122  2reu7  47123  2reu8  47124  2reuimp0  47126  ndmaovcom  47217  an4com24  47280  4an21  47282  sprvalpwn0  47470  prpair  47488  prproropf1olem0  47489  clnbgrel  47815  clnbgrsym  47824  2zrngnmrid  48172  rrx2linest  48663  pm5.32dav  48714  resinsnALT  48773  thincsect2  49115