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  1362  excxor  1516  cador  1608  cadcoma  1612  exancom  1861  19.42v  1953  19.42  2237  sbel2x  2472  eu6  2567  moanmo  2615  2eu3  2647  2eu7  2651  2eu8  2652  eq2tri  2791  r19.42v  3167  rexcomf  3275  rabswap  3412  spc2ed  3564  euxfr2w  3688  euxfr2  3690  rmo4  3698  reu8  3701  rmo3f  3702  reuxfrd  3716  rmo3  3849  difin2  4260  rcompleq  4264  euelss  4291  ssunsn  4788  uniprg  4883  inuni  5300  eqvinop  5442  elxp2  5655  opeliun2xp  5699  elvvv  5707  brinxp2  5709  dmuni  5868  imadmrn  6030  asymref2  6078  cnvopab  6098  cnvxp  6118  xpdifid  6129  cnvcnvsn  6180  opswap  6190  mptpreima  6199  xpco  6250  dfpo2  6257  fncnv  6573  fnres  6627  mptfnf  6635  dff1o2  6787  f13dfv  7231  fliftcnv  7268  isoini  7295  elrnmpores  7507  ndmovcom  7556  uniuni  7718  opabex3rd  7924  mptmpoopabbrd  8038  mptmpoopabbrdOLD  8039  fsplit  8073  brtpos  8191  tposmpo  8219  oaord  8488  nnaord  8560  naddasslem1  8635  naddasslem2  8636  brinxper  8677  pmex  8781  mapsnend  8984  snmapen  8986  xpsnen  9002  xpcomco  9008  elfi2  9341  supmo  9379  infmo  9424  frind  9679  cp  9820  dfac5lem1  10052  dfac5lem2  10053  dfac2b  10060  kmlem3  10082  cflim3  10191  brdom7disj  10460  brdom6disj  10461  recmulnq  10893  lesub0  11671  wloglei  11686  creur  12156  indstr  12851  xmulcom  13202  xmulneg1  13205  xmulf  13208  iccneg  13409  fzrev  13524  injresinj  13725  rediv  15073  imdiv  15080  lenegsq  15263  o1lo1  15479  fsumcom2  15716  fsumcom  15717  fprodcom2  15926  fprodcom  15927  divalglem10  16348  smueqlem  16436  gcdcom  16459  lcmcom  16539  isprm2  16628  isprm7  16654  infpn2  16860  imasleval  17480  dfiso3  17711  posglbmo  18347  odulatb  18369  oduclatb  18442  oppgid  19264  gsumcom  19883  gsumcom3  19884  dfrhm2  20359  xrsdsreclb  21306  opsrtoslem1  21938  psdmvr  22032  madutpos  22505  fvmptnn04if  22712  ntreq0  22940  ist0-3  23208  txkgen  23515  trfil2  23750  flimrest  23846  blres  24295  metrest  24388  restmetu  24434  elii1  24807  isclmp  24973  evthicc2  25337  ovolfcl  25343  dyaddisj  25473  iblpos  25670  itgposval  25673  ditgsplit  25738  itgsubst  25932  sincosq3sgn  26385  cos11  26418  dvdsflsumcom  27074  fsumvma  27100  logfaclbnd  27109  dchrelbas3  27125  lgsdi  27221  lgsquadlem3  27269  2lgslem1a  27278  sletri3  27643  nocvxmin  27666  sltrec  27708  istrkg2ld  28363  tgjustf  28376  tgcgr4  28434  mirreu3  28557  hpgcom  28670  colhp  28673  dfcgra2  28733  nbgrel  29243  nbgrsym  29266  wlkson  29558  dfpth2  29632  isspthonpth  29652  usgr2pth0  29668  wwlksnextinj  29802  elwspths2spth  29870  rusgrnumwwlkl1  29871  clwwlknclwwlkdifnum  29882  clwwlkn1  29943  clwwlkn2  29946  iseupthf1o  30104  eupth2lem2  30121  frgrncvvdeqlem2  30202  fusgr2wsp2nb  30236  fusgreg2wsp  30238  frgrreg  30296  frgrregord013  30297  h2hcau  30881  nmopub  31810  nmfnleub  31827  chrelati  32266  cvexchlem  32270  mdsymlem8  32312  sumdmdii  32317  13an22anass  32366  2reucom  32382  reuxfrdf  32393  dmrab  32399  difrab2  32400  ressupprn  32586  2ndpreima  32604  fpwrelmapffslem  32628  xrofsup  32663  sgn3da  32732  mgccnv  32898  pmtrprfv2  33018  smatrcl  33759  cnvordtrestixx  33876  issgon  34086  eulerpartlemr  34338  eulerpartlemgvv  34340  ballotlem2  34453  oddprm2  34619  bnj257  34670  bnj545  34858  bnj594  34875  nfan1c  35036  satfv0  35318  satfvsuclem1  35319  dfdm5  35733  dfrn5  35734  elima4  35736  elfix  35864  dffix2  35866  brimg  35898  brsuccf  35902  dfrecs2  35911  dfrdg4  35912  cgrcomlr  35959  ofscom  35968  btwnexch  35986  fscgr  36041  bj-df-ifc  36541  bj-dfmpoa  37079  bj-eldiag  37137  bj-imdirco  37151  bj-ccinftydisj  37174  mptsnunlem  37299  topdifinffinlem  37308  fvineqsneq  37373  wl-cases2-dnf  37473  wl-ax11-lem4  37549  fin2solem  37573  poimirlem26  37613  poimirlem30  37617  poimirlem32  37619  ftc1anclem6  37665  ftc1anc  37668  heibor1  37777  isdrngo3  37926  isdmn3  38041  anan  38190  br1cnvinxp  38218  inxpxrn  38354  prtlem70  38823  lrelat  38980  islshpat  38983  atlrelat1  39287  ishlat2  39319  cdlemb3  40573  diblsmopel  41138  dicelval3  41147  diclspsn  41161  uzindd  41938  3factsumint2  41983  3factsumint3  41984  3factsumint  41986  fimgmcyc  42495  eu6w  42637  fz1eqin  42730  diophrex  42736  fphpd  42777  fzneg  42944  expdioph  42985  dford4  42991  lnr2i  43078  fgraphopab  43165  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  44257  uunT1p1  44743  uun132p1  44748  un2122  44752  uun2131p1  44754  uunT12p1  44762  uunT12p2  44763  uunT12p3  44764  uun2221  44775  uun2221p1  44776  uun2221p2  44777  3impdirp1  44778  ancomstVD  44827  icccncfext  45858  dvnmul  45914  dvmptfprodlem  45915  dvnprodlem2  45918  fourierdlem42  46120  fourierdlem83  46160  f1cof1b  47051  2reu3  47084  2reu7  47085  2reu8  47086  2reuimp0  47088  ndmaovcom  47179  an4com24  47242  4an21  47244  sprvalpwn0  47457  prpair  47475  prproropf1olem0  47476  clnbgrel  47802  clnbgrsym  47811  2zrngnmrid  48217  rrx2linest  48704  pm5.32dav  48755  resinsnALT  48834  catcinv  49361  thincsect2  49430  lmdfval  49611  cmdfval  49612