Theorem ancom 459

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

Syntax hints:   ↔ wb 205   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  ancomd  460  biancomi  461  biancomd  462  ancomst  463  pm4.71r  557  pm5.32ri  574  pm5.32rd  576  an2anr  634  bianassc  641  an12  643  an13  645  an42  655  andir  1006  cases2  1045  dfifp6  1066  ifpn  1071  excxor  1509  cador  1601  cadcoma  1605  exancom  1856  19.42v  1949  19.42  2224  sbel2x  2467  eu6  2562  moanmo  2610  2eu3  2642  2eu7  2646  2eu8  2647  eq2tri  2792  r19.42v  3180  rexcomf  3290  rabswap  3428  spc2ed  3585  euxfr2w  3712  euxfr2  3714  rmo4  3722  reu8  3725  rmo3f  3726  reuxfrd  3740  rmo3  3879  difin2  4290  rcompleq  4294  euelss  4321  ssunsn  4833  uniprg  4925  inuni  5346  eqvinop  5489  elxp2  5702  elvvv  5753  brinxp2  5755  dmuni  5917  imadmrn  6074  asymref2  6124  cnvopab  6144  cnvxp  6163  xpdifid  6174  cnvcnvsn  6225  opswap  6235  mptpreima  6244  xpco  6295  dfpo2  6302  fncnv  6627  fnres  6683  mptfnf  6691  dff1o2  6843  f13dfv  7283  fliftcnv  7318  isoini  7345  elrnmpores  7559  ndmovcom  7608  uniuni  7765  opabex3rd  7971  mptmpoopabbrd  8085  mptmpoopabbrdOLD  8086  mptmpoopabbrdOLDOLD  8088  fsplit  8122  brtpos  8241  tposmpo  8269  oaord  8568  nnaord  8640  naddasslem1  8715  naddasslem2  8716  pmex  8850  mapsnend  9061  snmapen  9063  xpsnen  9080  xpcomco  9087  elfi2  9439  supmo  9477  infmo  9520  frind  9775  cp  9916  dfac5lem1  10148  dfac5lem2  10149  dfac2b  10155  kmlem3  10177  cflim3  10287  brdom7disj  10556  brdom6disj  10557  recmulnq  10989  lesub0  11763  wloglei  11778  creur  12239  indstr  12933  xmulcom  13280  xmulneg1  13283  xmulf  13286  iccneg  13484  fzrev  13599  injresinj  13789  rediv  15114  imdiv  15121  lenegsq  15303  o1lo1  15517  fsumcom2  15756  fsumcom  15757  fprodcom2  15964  fprodcom  15965  divalglem10  16382  smueqlem  16468  gcdcom  16491  lcmcom  16567  isprm2  16656  isprm7  16682  infpn2  16885  imasleval  17526  dfiso3  17759  posglbmo  18407  odulatb  18429  oduclatb  18502  oppgid  19322  gsumcom  19944  gsumcom3  19945  dfrhm2  20425  xrsdsreclb  21363  opsrtoslem1  22021  madutpos  22588  fvmptnn04if  22795  ntreq0  23025  ist0-3  23293  txkgen  23600  trfil2  23835  flimrest  23931  blres  24381  metrest  24477  restmetu  24523  elii1  24902  isclmp  25068  evthicc2  25433  ovolfcl  25439  dyaddisj  25569  iblpos  25766  itgposval  25769  ditgsplit  25834  itgsubst  26028  sincosq3sgn  26480  cos11  26512  dvdsflsumcom  27165  fsumvma  27191  logfaclbnd  27200  dchrelbas3  27216  lgsdi  27312  lgsquadlem3  27360  2lgslem1a  27369  sletri3  27734  nocvxmin  27757  sltrec  27799  istrkg2ld  28336  tgjustf  28349  tgcgr4  28407  mirreu3  28530  hpgcom  28643  colhp  28646  dfcgra2  28706  nbgrel  29225  nbgrsym  29248  wlkson  29542  isspthonpth  29635  usgr2pth0  29651  wwlksnextinj  29782  elwspths2spth  29850  rusgrnumwwlkl1  29851  clwwlknclwwlkdifnum  29862  clwwlkn1  29923  clwwlkn2  29926  iseupthf1o  30084  eupth2lem2  30101  frgrncvvdeqlem2  30182  fusgr2wsp2nb  30216  fusgreg2wsp  30218  frgrreg  30276  frgrregord013  30277  h2hcau  30861  nmopub  31790  nmfnleub  31807  chrelati  32246  cvexchlem  32250  mdsymlem8  32292  sumdmdii  32297  13an22anass  32342  2reucom  32356  reuxfrdf  32367  dmrab  32373  difrab2  32374  ressupprn  32552  2ndpreima  32569  fpwrelmapffslem  32596  xrofsup  32619  mgccnv  32815  pmtrprfv2  32901  smatrcl  33525  cnvordtrestixx  33642  issgon  33870  eulerpartlemr  34122  eulerpartlemgvv  34124  ballotlem2  34236  sgn3da  34289  oddprm2  34415  bnj257  34466  bnj545  34654  bnj594  34671  satfv0  35096  satfvsuclem1  35097  dfdm5  35496  dfrn5  35497  elima4  35499  elfix  35627  dffix2  35629  brimg  35661  brsuccf  35665  dfrecs2  35674  dfrdg4  35675  cgrcomlr  35722  ofscom  35731  btwnexch  35749  fscgr  35804  bj-df-ifc  36184  bj-dfmpoa  36725  bj-eldiag  36783  bj-imdirco  36797  bj-ccinftydisj  36820  mptsnunlem  36945  topdifinffinlem  36954  fvineqsneq  37019  wl-cases2-dnf  37107  wl-ax11-lem4  37183  fin2solem  37207  poimirlem26  37247  poimirlem30  37251  poimirlem32  37253  ftc1anclem6  37299  ftc1anc  37302  heibor1  37411  isdrngo3  37560  isdmn3  37675  anan  37826  br1cnvinxp  37855  inxpxrn  37994  prtlem70  38456  lrelat  38613  islshpat  38616  atlrelat1  38920  ishlat2  38952  cdlemb3  40206  diblsmopel  40771  dicelval3  40780  diclspsn  40794  uzindd  41576  3factsumint2  41622  3factsumint3  41623  3factsumint  41625  eu6w  42233  fz1eqin  42328  diophrex  42334  fphpd  42375  fzneg  42542  expdioph  42583  dford4  42589  lnr2i  42679  fgraphopab  42770  omge2  42866  oadif1lem  42947  oadif1  42948  ifpancor  43033  ifpidg  43060  ifpid2g  43062  ifpid1g  43063  ifpim23g  43064  rp-fakeoranass  43083  minregex  43103  dfid7  43181  dfrtrcl5  43198  relexp0eq  43270  fsovrfovd  43578  rr-grothprimbi  43871  uunT1p1  44359  uun132p1  44364  un2122  44368  uun2131p1  44370  uunT12p1  44378  uunT12p2  44379  uunT12p3  44380  uun2221  44391  uun2221p1  44392  uun2221p2  44393  3impdirp1  44394  ancomstVD  44443  icccncfext  45410  dvnmul  45466  dvmptfprodlem  45467  dvnprodlem2  45470  fourierdlem42  45672  fourierdlem83  45712  f1cof1b  46592  2reu3  46625  2reu7  46626  2reu8  46627  2reuimp0  46629  ndmaovcom  46720  an4com24  46783  4an21  46785  sprvalpwn0  46957  prpair  46975  prproropf1olem0  46976  clnbgrel  47301  clnbgrsym  47310  gricer  47373  2zrngnmrid  47501  opeliun2xp  47579  rrx2linest  47998  pm5.32dav  48049  iscnrm3lem3  48137  thincsect2  48247