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  4anpull2  1361  excxor  1515  cador  1607  cadcoma  1611  exancom  1860  19.42v  1952  19.42  2235  sbel2x  2477  eu6  2572  moanmo  2620  2eu3  2652  2eu7  2656  2eu8  2657  eq2tri  2796  r19.42v  3178  rexcomf  3286  rabswap  3429  spc2ed  3584  euxfr2w  3708  euxfr2  3710  rmo4  3718  reu8  3721  rmo3f  3722  reuxfrd  3736  rmo3  3869  difin2  4281  rcompleq  4285  euelss  4312  ssunsn  4808  uniprg  4903  inuni  5330  eqvinop  5472  elxp2  5689  opeliun2xp  5733  elvvv  5741  brinxp2  5743  dmuni  5905  imadmrn  6068  asymref2  6117  cnvopab  6137  cnvxp  6157  xpdifid  6168  cnvcnvsn  6219  opswap  6229  mptpreima  6238  xpco  6289  dfpo2  6296  fncnv  6619  fnres  6675  mptfnf  6683  dff1o2  6833  f13dfv  7276  fliftcnv  7313  isoini  7340  elrnmpores  7553  ndmovcom  7602  uniuni  7764  opabex3rd  7973  mptmpoopabbrd  8087  mptmpoopabbrdOLD  8088  mptmpoopabbrdOLDOLD  8090  fsplit  8124  brtpos  8242  tposmpo  8270  oaord  8567  nnaord  8639  naddasslem1  8714  naddasslem2  8715  brinxper  8756  pmex  8853  mapsnend  9058  snmapen  9060  xpsnen  9077  xpcomco  9084  elfi2  9436  supmo  9474  infmo  9517  frind  9772  cp  9913  dfac5lem1  10145  dfac5lem2  10146  dfac2b  10153  kmlem3  10175  cflim3  10284  brdom7disj  10553  brdom6disj  10554  recmulnq  10986  lesub0  11762  wloglei  11777  creur  12242  indstr  12940  xmulcom  13290  xmulneg1  13293  xmulf  13296  iccneg  13494  fzrev  13609  injresinj  13809  rediv  15152  imdiv  15159  lenegsq  15341  o1lo1  15555  fsumcom2  15792  fsumcom  15793  fprodcom2  16002  fprodcom  16003  divalglem10  16421  smueqlem  16509  gcdcom  16532  lcmcom  16612  isprm2  16701  isprm7  16727  infpn2  16933  imasleval  17557  dfiso3  17788  posglbmo  18426  odulatb  18448  oduclatb  18521  oppgid  19343  gsumcom  19963  gsumcom3  19964  dfrhm2  20442  xrsdsreclb  21393  opsrtoslem1  22027  psdmvr  22121  madutpos  22596  fvmptnn04if  22803  ntreq0  23031  ist0-3  23299  txkgen  23606  trfil2  23841  flimrest  23937  blres  24386  metrest  24481  restmetu  24527  elii1  24900  isclmp  25066  evthicc2  25431  ovolfcl  25437  dyaddisj  25567  iblpos  25764  itgposval  25767  ditgsplit  25832  itgsubst  26026  sincosq3sgn  26478  cos11  26511  dvdsflsumcom  27167  fsumvma  27193  logfaclbnd  27202  dchrelbas3  27218  lgsdi  27314  lgsquadlem3  27362  2lgslem1a  27371  sletri3  27736  nocvxmin  27759  sltrec  27801  istrkg2ld  28404  tgjustf  28417  tgcgr4  28475  mirreu3  28598  hpgcom  28711  colhp  28714  dfcgra2  28774  nbgrel  29285  nbgrsym  29308  wlkson  29602  dfpth2  29677  isspthonpth  29697  usgr2pth0  29713  wwlksnextinj  29847  elwspths2spth  29915  rusgrnumwwlkl1  29916  clwwlknclwwlkdifnum  29927  clwwlkn1  29988  clwwlkn2  29991  iseupthf1o  30149  eupth2lem2  30166  frgrncvvdeqlem2  30247  fusgr2wsp2nb  30281  fusgreg2wsp  30283  frgrreg  30341  frgrregord013  30342  h2hcau  30926  nmopub  31855  nmfnleub  31872  chrelati  32311  cvexchlem  32315  mdsymlem8  32357  sumdmdii  32362  13an22anass  32411  2reucom  32427  reuxfrdf  32438  dmrab  32444  difrab2  32445  ressupprn  32634  2ndpreima  32652  fpwrelmapffslem  32678  xrofsup  32708  mgccnv  32928  pmtrprfv2  33047  smatrcl  33754  cnvordtrestixx  33871  issgon  34083  eulerpartlemr  34335  eulerpartlemgvv  34337  ballotlem2  34450  sgn3da  34503  oddprm2  34629  bnj257  34680  bnj545  34868  bnj594  34885  nfan1c  35046  satfv0  35322  satfvsuclem1  35323  dfdm5  35732  dfrn5  35733  elima4  35735  elfix  35863  dffix2  35865  brimg  35897  brsuccf  35901  dfrecs2  35910  dfrdg4  35911  cgrcomlr  35958  ofscom  35967  btwnexch  35985  fscgr  36040  bj-df-ifc  36540  bj-dfmpoa  37078  bj-eldiag  37136  bj-imdirco  37150  bj-ccinftydisj  37173  mptsnunlem  37298  topdifinffinlem  37307  fvineqsneq  37372  wl-cases2-dnf  37472  wl-ax11-lem4  37548  fin2solem  37572  poimirlem26  37612  poimirlem30  37616  poimirlem32  37618  ftc1anclem6  37664  ftc1anc  37667  heibor1  37776  isdrngo3  37925  isdmn3  38040  anan  38189  br1cnvinxp  38216  inxpxrn  38355  prtlem70  38817  lrelat  38974  islshpat  38977  atlrelat1  39281  ishlat2  39313  cdlemb3  40567  diblsmopel  41132  dicelval3  41141  diclspsn  41155  uzindd  41937  3factsumint2  41982  3factsumint3  41983  3factsumint  41985  fimgmcyc  42507  eu6w  42649  fz1eqin  42743  diophrex  42749  fphpd  42790  fzneg  42957  expdioph  42998  dford4  43004  lnr2i  43091  fgraphopab  43178  omge2  43273  oadif1lem  43354  oadif1  43355  ifpancor  43439  ifpidg  43466  ifpid2g  43468  ifpid1g  43469  ifpim23g  43470  rp-fakeoranass  43489  minregex  43509  dfid7  43587  dfrtrcl5  43604  relexp0eq  43676  fsovrfovd  43984  rr-grothprimbi  44271  uunT1p1  44758  uun132p1  44763  un2122  44767  uun2131p1  44769  uunT12p1  44777  uunT12p2  44778  uunT12p3  44779  uun2221  44790  uun2221p1  44791  uun2221p2  44792  3impdirp1  44793  ancomstVD  44842  icccncfext  45859  dvnmul  45915  dvmptfprodlem  45916  dvnprodlem2  45919  fourierdlem42  46121  fourierdlem83  46161  f1cof1b  47047  2reu3  47080  2reu7  47081  2reu8  47082  2reuimp0  47084  ndmaovcom  47175  an4com24  47238  4an21  47240  sprvalpwn0  47428  prpair  47446  prproropf1olem0  47447  clnbgrel  47773  clnbgrsym  47782  2zrngnmrid  48130  rrx2linest  48621  pm5.32dav  48672  resinsnALT  48732  thincsect2  49093