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  3410  spc2ed  3557  euxfr2w  3680  euxfr2  3682  rmo4  3690  reu8  3693  rmo3f  3694  reuxfrd  3708  rmo3  3841  difin2  4255  rcompleq  4259  euelss  4286  ssunsn  4786  uniprg  4881  inuni  5297  eqvinop  5443  elxp2  5656  opeliun2xp  5700  elvvv  5708  brinxp2  5710  dmuni  5871  imadmrn  6037  asymref2  6082  cnvopab  6102  cnvxp  6123  xpdifid  6134  cnvcnvsn  6185  opswap  6195  mptpreima  6204  xpco  6255  dfpo2  6262  fncnv  6573  fnres  6627  mptfnf  6635  dff1o2  6787  f13dfv  7230  fliftcnv  7267  isoini  7294  elrnmpores  7506  ndmovcom  7555  uniuni  7717  opabex3rd  7920  mptmpoopabbrd  8034  mptmpoopabbrdOLD  8035  fsplit  8069  brtpos  8187  tposmpo  8215  oaord  8484  nnaord  8557  naddasslem1  8632  naddasslem2  8633  brinxper  8675  pmex  8780  mapsnend  8985  snmapen  8987  xpsnen  9001  xpcomco  9007  elfi2  9329  supmo  9367  infmo  9412  frind  9674  cp  9815  dfac5lem1  10045  dfac5lem2  10046  dfac2b  10053  kmlem3  10075  cflim3  10184  brdom7disj  10453  brdom6disj  10454  recmulnq  10887  lesub0  11666  wloglei  11681  creur  12151  indstr  12841  xmulcom  13193  xmulneg1  13196  xmulf  13199  iccneg  13400  fzrev  13515  injresinj  13719  rediv  15066  imdiv  15073  lenegsq  15256  o1lo1  15472  fsumcom2  15709  fsumcom  15710  fprodcom2  15919  fprodcom  15920  divalglem10  16341  smueqlem  16429  gcdcom  16452  lcmcom  16532  isprm2  16621  isprm7  16647  infpn2  16853  imasleval  17474  dfiso3  17709  posglbmo  18345  odulatb  18369  oduclatb  18442  oppgid  19297  gsumcom  19918  gsumcom3  19919  dfrhm2  20422  xrsdsreclb  21380  opsrtoslem1  22022  psdmvr  22124  madutpos  22598  fvmptnn04if  22805  ntreq0  23033  ist0-3  23301  txkgen  23608  trfil2  23843  flimrest  23939  blres  24387  metrest  24480  restmetu  24526  elii1  24899  isclmp  25065  evthicc2  25429  ovolfcl  25435  dyaddisj  25565  iblpos  25762  itgposval  25765  ditgsplit  25830  itgsubst  26024  sincosq3sgn  26477  cos11  26510  dvdsflsumcom  27166  fsumvma  27192  logfaclbnd  27201  dchrelbas3  27217  lgsdi  27313  lgsquadlem3  27361  2lgslem1a  27370  lestri3  27735  ltsrec  27809  istrkg2ld  28544  tgjustf  28557  tgcgr4  28615  mirreu3  28738  hpgcom  28851  colhp  28854  dfcgra2  28914  nbgrel  29425  nbgrsym  29448  wlkson  29740  dfpth2  29814  isspthonpth  29834  usgr2pth0  29850  wwlksnextinj  29984  elwspths2spth  30055  rusgrnumwwlkl1  30056  clwwlknclwwlkdifnum  30067  clwwlkn1  30128  clwwlkn2  30131  iseupthf1o  30289  eupth2lem2  30306  frgrncvvdeqlem2  30387  fusgr2wsp2nb  30421  fusgreg2wsp  30423  frgrreg  30481  frgrregord013  30482  h2hcau  31067  nmopub  31996  nmfnleub  32013  chrelati  32452  cvexchlem  32456  mdsymlem8  32498  sumdmdii  32503  13an22anass  32550  2reucom  32566  reuxfrdf  32577  dmrab  32583  difrab2  32584  ressupprn  32780  2ndpreima  32798  fpwrelmapffslem  32822  xrofsup  32858  sgn3da  32926  mgccnv  33092  pmtrprfv2  33182  smatrcl  33974  cnvordtrestixx  34091  issgon  34301  eulerpartlemr  34552  eulerpartlemgvv  34554  ballotlem2  34667  oddprm2  34833  bnj257  34884  bnj545  35071  bnj594  35088  nfan1c  35249  satfv0  35574  satfvsuclem1  35575  dfdm5  35989  dfrn5  35990  elima4  35992  elfix  36117  dffix2  36119  brimg  36151  lemsuccf  36155  dfrecs2  36166  dfrdg4  36167  cgrcomlr  36214  ofscom  36223  btwnexch  36241  fscgr  36296  bj-df-ifc  36805  bj-axseprep  37322  bj-dfmpoa  37371  bj-eldiag  37431  bj-imdirco  37445  bj-ccinftydisj  37468  mptsnunlem  37593  topdifinffinlem  37602  fvineqsneq  37667  wl-cases2-dnf  37767  fin2solem  37857  poimirlem26  37897  poimirlem30  37901  poimirlem32  37903  ftc1anclem6  37949  ftc1anc  37952  heibor1  38061  isdrngo3  38210  isdmn3  38325  anan  38486  br1cnvinxp  38510  raldmqseu  38616  inxpxrn  38669  prtlem70  39233  lrelat  39390  islshpat  39393  atlrelat1  39697  ishlat2  39729  cdlemb3  40982  diblsmopel  41547  dicelval3  41556  diclspsn  41570  uzindd  42347  3factsumint2  42392  3factsumint3  42393  3factsumint  42395  fimgmcyc  42904  eu6w  43034  fz1eqin  43126  diophrex  43132  fphpd  43173  fzneg  43339  expdioph  43380  dford4  43386  lnr2i  43473  fgraphopab  43560  omge2  43655  oadif1lem  43736  oadif1  43737  ifpancor  43820  ifpidg  43847  ifpid2g  43849  ifpid1g  43850  ifpim23g  43851  rp-fakeoranass  43870  minregex  43890  dfid7  43968  dfrtrcl5  43985  relexp0eq  44057  fsovrfovd  44365  rr-grothprimbi  44651  uunT1p1  45136  uun132p1  45141  un2122  45145  uun2131p1  45147  uunT12p1  45155  uunT12p2  45156  uunT12p3  45157  uun2221  45168  uun2221p1  45169  uun2221p2  45170  3impdirp1  45171  ancomstVD  45220  icccncfext  46245  dvnmul  46301  dvmptfprodlem  46302  dvnprodlem2  46305  fourierdlem42  46507  fourierdlem83  46547  f1cof1b  47437  2reu3  47470  2reu7  47471  2reu8  47472  2reuimp0  47474  ndmaovcom  47565  an4com24  47628  4an21  47630  sprvalpwn0  47843  prpair  47861  prproropf1olem0  47862  clnbgrel  48188  clnbgrsym  48198  2zrngnmrid  48616  rrx2linest  49102  pm5.32dav  49153  resinsnALT  49232  catcinv  49758  thincsect2  49827  lmdfval  50008  cmdfval  50009