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  1517  cador  1609  cadcoma  1613  exancom  1862  19.42v  1954  19.42  2241  sbel2x  2476  eu6  2571  moanmo  2619  2eu3  2651  2eu7  2655  2eu8  2656  eq2tri  2795  r19.42v  3165  rexcomf  3272  rabswap  3405  spc2ed  3552  euxfr2w  3675  euxfr2  3677  rmo4  3685  reu8  3688  rmo3f  3689  reuxfrd  3703  rmo3  3836  difin2  4250  rcompleq  4254  euelss  4281  ssunsn  4781  uniprg  4876  inuni  5292  eqvinop  5432  elxp2  5645  opeliun2xp  5689  elvvv  5697  brinxp2  5699  dmuni  5860  imadmrn  6026  asymref2  6071  cnvopab  6091  cnvxp  6112  xpdifid  6123  cnvcnvsn  6174  opswap  6184  mptpreima  6193  xpco  6244  dfpo2  6251  fncnv  6562  fnres  6616  mptfnf  6624  dff1o2  6776  f13dfv  7217  fliftcnv  7254  isoini  7281  elrnmpores  7493  ndmovcom  7542  uniuni  7704  opabex3rd  7907  mptmpoopabbrd  8021  mptmpoopabbrdOLD  8022  fsplit  8056  brtpos  8174  tposmpo  8202  oaord  8471  nnaord  8543  naddasslem1  8618  naddasslem2  8619  brinxper  8660  pmex  8764  mapsnend  8969  snmapen  8971  xpsnen  8985  xpcomco  8991  elfi2  9309  supmo  9347  infmo  9392  frind  9654  cp  9795  dfac5lem1  10025  dfac5lem2  10026  dfac2b  10033  kmlem3  10055  cflim3  10164  brdom7disj  10433  brdom6disj  10434  recmulnq  10866  lesub0  11645  wloglei  11660  creur  12130  indstr  12820  xmulcom  13172  xmulneg1  13175  xmulf  13178  iccneg  13379  fzrev  13494  injresinj  13698  rediv  15045  imdiv  15052  lenegsq  15235  o1lo1  15451  fsumcom2  15688  fsumcom  15689  fprodcom2  15898  fprodcom  15899  divalglem10  16320  smueqlem  16408  gcdcom  16431  lcmcom  16511  isprm2  16600  isprm7  16626  infpn2  16832  imasleval  17453  dfiso3  17688  posglbmo  18324  odulatb  18348  oduclatb  18421  oppgid  19276  gsumcom  19897  gsumcom3  19898  dfrhm2  20401  xrsdsreclb  21359  opsrtoslem1  22001  psdmvr  22103  madutpos  22577  fvmptnn04if  22784  ntreq0  23012  ist0-3  23280  txkgen  23587  trfil2  23822  flimrest  23918  blres  24366  metrest  24459  restmetu  24505  elii1  24878  isclmp  25044  evthicc2  25408  ovolfcl  25414  dyaddisj  25544  iblpos  25741  itgposval  25744  ditgsplit  25809  itgsubst  26003  sincosq3sgn  26456  cos11  26489  dvdsflsumcom  27145  fsumvma  27171  logfaclbnd  27180  dchrelbas3  27196  lgsdi  27292  lgsquadlem3  27340  2lgslem1a  27349  sletri3  27714  sltrec  27782  istrkg2ld  28458  tgjustf  28471  tgcgr4  28529  mirreu3  28652  hpgcom  28765  colhp  28768  dfcgra2  28828  nbgrel  29339  nbgrsym  29362  wlkson  29654  dfpth2  29728  isspthonpth  29748  usgr2pth0  29764  wwlksnextinj  29898  elwspths2spth  29969  rusgrnumwwlkl1  29970  clwwlknclwwlkdifnum  29981  clwwlkn1  30042  clwwlkn2  30045  iseupthf1o  30203  eupth2lem2  30220  frgrncvvdeqlem2  30301  fusgr2wsp2nb  30335  fusgreg2wsp  30337  frgrreg  30395  frgrregord013  30396  h2hcau  30980  nmopub  31909  nmfnleub  31926  chrelati  32365  cvexchlem  32369  mdsymlem8  32411  sumdmdii  32416  13an22anass  32464  2reucom  32480  reuxfrdf  32491  dmrab  32497  difrab2  32498  ressupprn  32695  2ndpreima  32713  fpwrelmapffslem  32739  xrofsup  32775  sgn3da  32843  mgccnv  33009  pmtrprfv2  33098  smatrcl  33881  cnvordtrestixx  33998  issgon  34208  eulerpartlemr  34459  eulerpartlemgvv  34461  ballotlem2  34574  oddprm2  34740  bnj257  34791  bnj545  34979  bnj594  34996  nfan1c  35157  satfv0  35474  satfvsuclem1  35475  dfdm5  35889  dfrn5  35890  elima4  35892  elfix  36017  dffix2  36019  brimg  36051  lemsuccf  36055  dfrecs2  36066  dfrdg4  36067  cgrcomlr  36114  ofscom  36123  btwnexch  36141  fscgr  36196  bj-df-ifc  36696  bj-dfmpoa  37235  bj-eldiag  37293  bj-imdirco  37307  bj-ccinftydisj  37330  mptsnunlem  37455  topdifinffinlem  37464  fvineqsneq  37529  wl-cases2-dnf  37629  fin2solem  37719  poimirlem26  37759  poimirlem30  37763  poimirlem32  37765  ftc1anclem6  37811  ftc1anc  37814  heibor1  37923  isdrngo3  38072  isdmn3  38187  anan  38343  br1cnvinxp  38366  inxpxrn  38515  prtlem70  39029  lrelat  39186  islshpat  39189  atlrelat1  39493  ishlat2  39525  cdlemb3  40778  diblsmopel  41343  dicelval3  41352  diclspsn  41366  uzindd  42143  3factsumint2  42188  3factsumint3  42189  3factsumint  42191  fimgmcyc  42704  eu6w  42834  fz1eqin  42926  diophrex  42932  fphpd  42973  fzneg  43139  expdioph  43180  dford4  43186  lnr2i  43273  fgraphopab  43360  omge2  43455  oadif1lem  43536  oadif1  43537  ifpancor  43621  ifpidg  43648  ifpid2g  43650  ifpid1g  43651  ifpim23g  43652  rp-fakeoranass  43671  minregex  43691  dfid7  43769  dfrtrcl5  43786  relexp0eq  43858  fsovrfovd  44166  rr-grothprimbi  44452  uunT1p1  44937  uun132p1  44942  un2122  44946  uun2131p1  44948  uunT12p1  44956  uunT12p2  44957  uunT12p3  44958  uun2221  44969  uun2221p1  44970  uun2221p2  44971  3impdirp1  44972  ancomstVD  45021  icccncfext  46047  dvnmul  46103  dvmptfprodlem  46104  dvnprodlem2  46107  fourierdlem42  46309  fourierdlem83  46349  f1cof1b  47239  2reu3  47272  2reu7  47273  2reu8  47274  2reuimp0  47276  ndmaovcom  47367  an4com24  47430  4an21  47432  sprvalpwn0  47645  prpair  47663  prproropf1olem0  47664  clnbgrel  47990  clnbgrsym  48000  2zrngnmrid  48418  rrx2linest  48904  pm5.32dav  48955  resinsnALT  49034  catcinv  49560  thincsect2  49629  lmdfval  49810  cmdfval  49811