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  577  an2anr  635  bianassc  642  an12  644  an13  646  an42  656  andir  1009  cases2  1048  dfifp6  1069  ifpn  1074  excxor  1513  cador  1605  cadcoma  1609  exancom  1860  19.42v  1953  19.42  2237  sbel2x  2482  eu6  2577  moanmo  2625  2eu3  2657  2eu7  2661  2eu8  2662  eq2tri  2807  r19.42v  3197  rexcomf  3309  rabswap  3453  spc2ed  3614  euxfr2w  3742  euxfr2  3744  rmo4  3752  reu8  3755  rmo3f  3756  reuxfrd  3770  rmo3  3911  difin2  4320  rcompleq  4324  euelss  4351  ssunsn  4853  uniprg  4947  inuni  5368  eqvinop  5507  elxp2  5724  elvvv  5775  brinxp2  5777  dmuni  5939  imadmrn  6099  asymref2  6149  cnvopab  6169  cnvxp  6188  xpdifid  6199  cnvcnvsn  6250  opswap  6260  mptpreima  6269  xpco  6320  dfpo2  6327  fncnv  6651  fnres  6707  mptfnf  6715  dff1o2  6867  f13dfv  7310  fliftcnv  7347  isoini  7374  elrnmpores  7588  ndmovcom  7637  uniuni  7797  opabex3rd  8007  mptmpoopabbrd  8121  mptmpoopabbrdOLD  8122  mptmpoopabbrdOLDOLD  8124  fsplit  8158  brtpos  8276  tposmpo  8304  oaord  8603  nnaord  8675  naddasslem1  8750  naddasslem2  8751  brinxper  8792  pmex  8889  mapsnend  9101  snmapen  9103  xpsnen  9121  xpcomco  9128  elfi2  9483  supmo  9521  infmo  9564  frind  9819  cp  9960  dfac5lem1  10192  dfac5lem2  10193  dfac2b  10200  kmlem3  10222  cflim3  10331  brdom7disj  10600  brdom6disj  10601  recmulnq  11033  lesub0  11807  wloglei  11822  creur  12287  indstr  12981  xmulcom  13328  xmulneg1  13331  xmulf  13334  iccneg  13532  fzrev  13647  injresinj  13838  rediv  15180  imdiv  15187  lenegsq  15369  o1lo1  15583  fsumcom2  15822  fsumcom  15823  fprodcom2  16032  fprodcom  16033  divalglem10  16450  smueqlem  16536  gcdcom  16559  lcmcom  16640  isprm2  16729  isprm7  16755  infpn2  16960  imasleval  17601  dfiso3  17834  posglbmo  18482  odulatb  18504  oduclatb  18577  oppgid  19399  gsumcom  20019  gsumcom3  20020  dfrhm2  20500  xrsdsreclb  21454  opsrtoslem1  22102  madutpos  22669  fvmptnn04if  22876  ntreq0  23106  ist0-3  23374  txkgen  23681  trfil2  23916  flimrest  24012  blres  24462  metrest  24558  restmetu  24604  elii1  24983  isclmp  25149  evthicc2  25514  ovolfcl  25520  dyaddisj  25650  iblpos  25848  itgposval  25851  ditgsplit  25916  itgsubst  26110  sincosq3sgn  26560  cos11  26593  dvdsflsumcom  27249  fsumvma  27275  logfaclbnd  27284  dchrelbas3  27300  lgsdi  27396  lgsquadlem3  27444  2lgslem1a  27453  sletri3  27818  nocvxmin  27841  sltrec  27883  istrkg2ld  28486  tgjustf  28499  tgcgr4  28557  mirreu3  28680  hpgcom  28793  colhp  28796  dfcgra2  28856  nbgrel  29375  nbgrsym  29398  wlkson  29692  isspthonpth  29785  usgr2pth0  29801  wwlksnextinj  29932  elwspths2spth  30000  rusgrnumwwlkl1  30001  clwwlknclwwlkdifnum  30012  clwwlkn1  30073  clwwlkn2  30076  iseupthf1o  30234  eupth2lem2  30251  frgrncvvdeqlem2  30332  fusgr2wsp2nb  30366  fusgreg2wsp  30368  frgrreg  30426  frgrregord013  30427  h2hcau  31011  nmopub  31940  nmfnleub  31957  chrelati  32396  cvexchlem  32400  mdsymlem8  32442  sumdmdii  32447  13an22anass  32493  2reucom  32508  reuxfrdf  32519  dmrab  32525  difrab2  32526  ressupprn  32702  2ndpreima  32719  fpwrelmapffslem  32746  xrofsup  32774  mgccnv  32972  pmtrprfv2  33081  smatrcl  33742  cnvordtrestixx  33859  issgon  34087  eulerpartlemr  34339  eulerpartlemgvv  34341  ballotlem2  34453  sgn3da  34506  oddprm2  34632  bnj257  34683  bnj545  34871  bnj594  34888  nfan1c  35049  satfv0  35326  satfvsuclem1  35327  dfdm5  35736  dfrn5  35737  elima4  35739  elfix  35867  dffix2  35869  brimg  35901  brsuccf  35905  dfrecs2  35914  dfrdg4  35915  cgrcomlr  35962  ofscom  35971  btwnexch  35989  fscgr  36044  bj-df-ifc  36546  bj-dfmpoa  37084  bj-eldiag  37142  bj-imdirco  37156  bj-ccinftydisj  37179  mptsnunlem  37304  topdifinffinlem  37313  fvineqsneq  37378  wl-cases2-dnf  37466  wl-ax11-lem4  37542  fin2solem  37566  poimirlem26  37606  poimirlem30  37610  poimirlem32  37612  ftc1anclem6  37658  ftc1anc  37661  heibor1  37770  isdrngo3  37919  isdmn3  38034  anan  38183  br1cnvinxp  38212  inxpxrn  38351  prtlem70  38813  lrelat  38970  islshpat  38973  atlrelat1  39277  ishlat2  39309  cdlemb3  40563  diblsmopel  41128  dicelval3  41137  diclspsn  41151  uzindd  41933  3factsumint2  41979  3factsumint3  41980  3factsumint  41982  fimgmcyc  42489  eu6w  42631  fz1eqin  42725  diophrex  42731  fphpd  42772  fzneg  42939  expdioph  42980  dford4  42986  lnr2i  43073  fgraphopab  43164  omge2  43260  oadif1lem  43341  oadif1  43342  ifpancor  43426  ifpidg  43453  ifpid2g  43455  ifpid1g  43456  ifpim23g  43457  rp-fakeoranass  43476  minregex  43496  dfid7  43574  dfrtrcl5  43591  relexp0eq  43663  fsovrfovd  43971  rr-grothprimbi  44264  uunT1p1  44752  uun132p1  44757  un2122  44761  uun2131p1  44763  uunT12p1  44771  uunT12p2  44772  uunT12p3  44773  uun2221  44784  uun2221p1  44785  uun2221p2  44786  3impdirp1  44787  ancomstVD  44836  icccncfext  45808  dvnmul  45864  dvmptfprodlem  45865  dvnprodlem2  45868  fourierdlem42  46070  fourierdlem83  46110  f1cof1b  46992  2reu3  47025  2reu7  47026  2reu8  47027  2reuimp0  47029  ndmaovcom  47120  an4com24  47183  4an21  47185  sprvalpwn0  47357  prpair  47375  prproropf1olem0  47376  clnbgrel  47701  clnbgrsym  47710  2zrngnmrid  47979  opeliun2xp  48057  rrx2linest  48476  pm5.32dav  48527  iscnrm3lem3  48615  thincsect2  48725