Theorem ancom 464

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 463	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜓 ∧ 𝜑))
2		pm3.22 463	. 2 ⊢ ((𝜓 ∧ 𝜑) → (𝜑 ∧ 𝜓))
3	1, 2	impbii 211	1 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜓 ∧ 𝜑))

Syntax hints:   ↔ wb 208   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  ancomd  465  biancomi  466  biancomd  467  ancomst  468  pm4.71r  566  pm5.32ri  583  pm5.32rd  586  an2anr  645  bianassc  653  an12  655  an13  657  an42  667  andir  1021  cases2  1058  dfifp6  1079  ifpn  1084  4anpull2  1374  excxor  1535  cador  1627  cadcoma  1631  exancom  1880  19.42v  1972  19.42  2270  sbel2x  2504  eu6  2600  moanmo  2648  2eu3  2679  2eu7  2683  2eu8  2684  eq2tri  2823  r19.42v  3193  rexcomf  3300  rabswap  3422  spc2ed  3559  euxfr2w  3681  euxfr2  3683  rmo4  3691  reu8  3694  rmo3f  3695  reuxfrd  3709  rmo3  3840  difin2  4251  rcompleq  4255  euelss  4282  ssunsn  4783  uniprg  4878  inuni  5303  eqvinop  5452  elxp2  5667  opeliun2xp  5711  elvvv  5719  brinxp2  5721  dmuni  5886  imadmrn  6055  asymref2  6100  cnvopab  6120  cnvxp  6138  xpdifid  6149  cnvcnvsn  6201  opswap  6211  mptpreima  6220  xpco  6271  dfpo2  6278  fncnv  6589  fnres  6643  mptfnf  6651  dff1o2  6807  f13dfv  7253  fliftcnv  7290  isoini  7317  elrnmpores  7529  ndmovcom  7578  uniuni  7740  opabex3rd  7942  mptmpoopabbrd  8056  fsplit  8090  brtpos  8209  tposmpo  8237  oaord  8510  nnaord  8583  naddasslem1  8659  naddasslem2  8660  brinxper  8702  pmex  8807  mapsnend  9011  snmapen  9013  xpsnen  9027  xpcomco  9033  elfi2  9354  supmo  9392  infmo  9437  frind  9702  cp  9843  dfac5lem1  10073  dfac5lem2  10074  dfac2b  10081  kmlem3  10103  cflim3  10213  brdom7disj  10482  brdom6disj  10483  recmulnq  10916  lesub0  11698  wloglei  11713  creur  12183  indstr  12911  xmulcom  13263  xmulneg1  13266  xmulf  13269  iccneg  13470  fzrev  13586  injresinj  13791  sgn3da  15105  rediv  15149  imdiv  15156  lenegsq  15339  o1lo1  15555  fsumcom2  15792  fsumcom  15793  fprodcom2  16005  fprodcom  16006  divalglem10  16427  smueqlem  16515  gcdcom  16538  lcmcom  16618  isprm2  16707  isprm7  16734  infpn2  16940  imasleval  17562  dfiso3  17797  posglbmo  18433  odulatb  18457  oduclatb  18530  oppgid  19387  gsumcom  20008  gsumcom3  20009  dfrhm2  20510  xrsdsreclb  21454  opsrtoslem1  22096  psdmvr  22222  madutpos  22690  fvmptnn04if  22897  ntreq0  23125  ist0-3  23393  txkgen  23700  trfil2  23935  flimrest  24031  blres  24479  metrest  24572  restmetu  24618  elii1  24985  isclmp  25147  evthicc2  25510  ovolfcl  25516  dyaddisj  25646  iblpos  25843  itgposval  25846  ditgsplit  25911  itgsubst  26099  sincosq3sgn  26553  cos11  26586  dvdsflsumcom  27240  fsumvma  27265  logfaclbnd  27274  dchrelbas3  27290  lgsdi  27386  lgsquadlem3  27434  2lgslem1a  27443  lestri3  27807  ltsrec  27882  istrkg2ld  28617  tgjustf  28630  tgcgr4  28688  mirreu3  28811  hpgcom  28924  colhp  28927  dfcgra2  28987  nbgrel  29498  nbgrsym  29521  wlkson  29812  dfpth2  29886  isspthonpth  29906  usgr2pth0  29922  wwlksnextinj  30056  elwspths2spth  30127  rusgrnumwwlkl1  30128  clwwlknclwwlkdifnum  30139  clwwlkn1  30200  clwwlkn2  30203  iseupthf1o  30361  eupth2lem2  30378  frgrncvvdeqlem2  30459  fusgr2wsp2nb  30493  fusgreg2wsp  30495  frgrreg  30553  frgrregord013  30554  h2hcau  31139  nmopub  32068  nmfnleub  32085  chrelati  32524  cvexchlem  32528  mdsymlem8  32570  sumdmdii  32575  13an22anass  32622  2reucom  32638  reuxfrdf  32649  dmrab  32655  difrab2  32656  ififcom  32709  ressupprn  32853  2ndpreima  32871  fpwrelmapffslem  32895  xrofsup  32930  mgccnv  33138  pmtrprfv2  33229  smatrcl  34054  cnvordtrestixx  34171  issgon  34381  eulerpartlemr  34632  eulerpartlemgvv  34634  ballotlem2  34747  oddprm2  34910  bnj257  34964  bnj545  35151  bnj594  35168  nfan1c  35329  satfv0  35669  satfvsuclem1  35670  dfdm5  36084  dfrn5  36085  elima4  36087  elfix  36212  dffix2  36214  brimg  36246  lemsuccf  36250  dfrecs2  36261  dfrdg4  36262  cgrcomlr  36309  ofscom  36318  btwnexch  36336  fscgr  36391  bj-df-ifc  36984  bj-axseprep  37520  bj-dfmpoa  37569  bj-eldiag  37629  bj-imdirco  37643  bj-ccinftydisj  37666  mptsnunlem  37793  topdifinffinlem  37802  fvineqsneq  37867  wl-cases2-dnf  37976  fin2solem  38066  poimirlem26  38106  poimirlem30  38110  poimirlem32  38112  ftc1anclem6  38158  ftc1anc  38161  heibor1  38270  isdrngo3  38419  isdmn3  38534  anan  38695  br1cnvinxp  38719  raldmqseu  38825  inxpxrn  38878  prtlem70  39442  lrelat  39599  islshpat  39602  atlrelat1  39906  ishlat2  39938  cdlemb3  41191  diblsmopel  41756  dicelval3  41765  diclspsn  41779  uzindd  42556  3factsumint2  42600  3factsumint3  42601  3factsumint  42603  fimgmcyc  43113  eu6w  43219  fz1eqin  43311  diophrex  43317  fphpd  43354  fzneg  43520  expdioph  43561  dford4  43567  lnr2i  43654  fgraphopab  43741  omge2  43836  oadif1lem  43917  oadif1  43918  ifpancor  44001  ifpidg  44028  ifpid2g  44030  ifpid1g  44031  ifpim23g  44032  rp-fakeoranass  44051  minregex  44071  dfid7  44149  dfrtrcl5  44166  relexp0eq  44238  fsovrfovd  44546  rr-grothprimbi  44832  uunT1p1  45317  uun132p1  45322  un2122  45326  uun2131p1  45328  uunT12p1  45336  uunT12p2  45337  uunT12p3  45338  uun2221  45349  uun2221p1  45350  uun2221p2  45351  3impdirp1  45352  ancomstVD  45401  icccncfext  46422  dvnmul  46478  dvmptfprodlem  46479  dvnprodlem2  46482  fourierdlem42  46684  fourierdlem83  46724  f1cof1b  47632  2reu3  47665  2reu7  47666  2reu8  47667  2reuimp0  47669  ndmaovcom  47760  an4com24  47823  4an21  47825  sprvalpwn0  48050  prpair  48068  prproropf1olem0  48069  clnbgrel  48411  clnbgrsym  48421  2zrngnmrid  48839  rrx2linest  49325  pm5.32dav  49376  resinsnALT  49455  catcinv  49981  thincsect2  50050  lmdfval  50231  cmdfval  50232