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  2236  sbel2x  2478  eu6  2573  moanmo  2621  2eu3  2653  2eu7  2657  2eu8  2658  eq2tri  2797  r19.42v  3176  rexcomf  3283  rabswap  3425  spc2ed  3580  euxfr2w  3703  euxfr2  3705  rmo4  3713  reu8  3716  rmo3f  3717  reuxfrd  3731  rmo3  3864  difin2  4276  rcompleq  4280  euelss  4307  ssunsn  4804  uniprg  4899  inuni  5320  eqvinop  5462  elxp2  5678  opeliun2xp  5722  elvvv  5730  brinxp2  5732  dmuni  5894  imadmrn  6057  asymref2  6106  cnvopab  6126  cnvxp  6146  xpdifid  6157  cnvcnvsn  6208  opswap  6218  mptpreima  6227  xpco  6278  dfpo2  6285  fncnv  6608  fnres  6664  mptfnf  6672  dff1o2  6822  f13dfv  7266  fliftcnv  7303  isoini  7330  elrnmpores  7543  ndmovcom  7592  uniuni  7754  opabex3rd  7963  mptmpoopabbrd  8077  mptmpoopabbrdOLD  8078  mptmpoopabbrdOLDOLD  8080  fsplit  8114  brtpos  8232  tposmpo  8260  oaord  8557  nnaord  8629  naddasslem1  8704  naddasslem2  8705  brinxper  8746  pmex  8843  mapsnend  9048  snmapen  9050  xpsnen  9067  xpcomco  9074  elfi2  9424  supmo  9462  infmo  9507  frind  9762  cp  9903  dfac5lem1  10135  dfac5lem2  10136  dfac2b  10143  kmlem3  10165  cflim3  10274  brdom7disj  10543  brdom6disj  10544  recmulnq  10976  lesub0  11752  wloglei  11767  creur  12232  indstr  12930  xmulcom  13280  xmulneg1  13283  xmulf  13286  iccneg  13487  fzrev  13602  injresinj  13802  rediv  15148  imdiv  15155  lenegsq  15337  o1lo1  15551  fsumcom2  15788  fsumcom  15789  fprodcom2  15998  fprodcom  15999  divalglem10  16419  smueqlem  16507  gcdcom  16530  lcmcom  16610  isprm2  16699  isprm7  16725  infpn2  16931  imasleval  17553  dfiso3  17784  posglbmo  18420  odulatb  18442  oduclatb  18515  oppgid  19337  gsumcom  19956  gsumcom3  19957  dfrhm2  20432  xrsdsreclb  21379  opsrtoslem1  22011  psdmvr  22105  madutpos  22578  fvmptnn04if  22785  ntreq0  23013  ist0-3  23281  txkgen  23588  trfil2  23823  flimrest  23919  blres  24368  metrest  24461  restmetu  24507  elii1  24880  isclmp  25046  evthicc2  25411  ovolfcl  25417  dyaddisj  25547  iblpos  25744  itgposval  25747  ditgsplit  25812  itgsubst  26006  sincosq3sgn  26459  cos11  26492  dvdsflsumcom  27148  fsumvma  27174  logfaclbnd  27183  dchrelbas3  27199  lgsdi  27295  lgsquadlem3  27343  2lgslem1a  27352  sletri3  27717  nocvxmin  27740  sltrec  27782  istrkg2ld  28385  tgjustf  28398  tgcgr4  28456  mirreu3  28579  hpgcom  28692  colhp  28695  dfcgra2  28755  nbgrel  29265  nbgrsym  29288  wlkson  29582  dfpth2  29657  isspthonpth  29677  usgr2pth0  29693  wwlksnextinj  29827  elwspths2spth  29895  rusgrnumwwlkl1  29896  clwwlknclwwlkdifnum  29907  clwwlkn1  29968  clwwlkn2  29971  iseupthf1o  30129  eupth2lem2  30146  frgrncvvdeqlem2  30227  fusgr2wsp2nb  30261  fusgreg2wsp  30263  frgrreg  30321  frgrregord013  30322  h2hcau  30906  nmopub  31835  nmfnleub  31852  chrelati  32291  cvexchlem  32295  mdsymlem8  32337  sumdmdii  32342  13an22anass  32391  2reucom  32407  reuxfrdf  32418  dmrab  32424  difrab2  32425  ressupprn  32613  2ndpreima  32631  fpwrelmapffslem  32655  xrofsup  32690  sgn3da  32759  mgccnv  32925  pmtrprfv2  33045  smatrcl  33773  cnvordtrestixx  33890  issgon  34100  eulerpartlemr  34352  eulerpartlemgvv  34354  ballotlem2  34467  oddprm2  34633  bnj257  34684  bnj545  34872  bnj594  34889  nfan1c  35050  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  36544  bj-dfmpoa  37082  bj-eldiag  37140  bj-imdirco  37154  bj-ccinftydisj  37177  mptsnunlem  37302  topdifinffinlem  37311  fvineqsneq  37376  wl-cases2-dnf  37476  wl-ax11-lem4  37552  fin2solem  37576  poimirlem26  37616  poimirlem30  37620  poimirlem32  37622  ftc1anclem6  37668  ftc1anc  37671  heibor1  37780  isdrngo3  37929  isdmn3  38044  anan  38193  br1cnvinxp  38220  inxpxrn  38359  prtlem70  38821  lrelat  38978  islshpat  38981  atlrelat1  39285  ishlat2  39317  cdlemb3  40571  diblsmopel  41136  dicelval3  41145  diclspsn  41159  uzindd  41936  3factsumint2  41981  3factsumint3  41982  3factsumint  41984  fimgmcyc  42504  eu6w  42646  fz1eqin  42739  diophrex  42745  fphpd  42786  fzneg  42953  expdioph  42994  dford4  43000  lnr2i  43087  fgraphopab  43174  omge2  43269  oadif1lem  43350  oadif1  43351  ifpancor  43435  ifpidg  43462  ifpid2g  43464  ifpid1g  43465  ifpim23g  43466  rp-fakeoranass  43485  minregex  43505  dfid7  43583  dfrtrcl5  43600  relexp0eq  43672  fsovrfovd  43980  rr-grothprimbi  44267  uunT1p1  44753  uun132p1  44758  un2122  44762  uun2131p1  44764  uunT12p1  44772  uunT12p2  44773  uunT12p3  44774  uun2221  44785  uun2221p1  44786  uun2221p2  44787  3impdirp1  44788  ancomstVD  44837  icccncfext  45864  dvnmul  45920  dvmptfprodlem  45921  dvnprodlem2  45924  fourierdlem42  46126  fourierdlem83  46166  f1cof1b  47054  2reu3  47087  2reu7  47088  2reu8  47089  2reuimp0  47091  ndmaovcom  47182  an4com24  47245  4an21  47247  sprvalpwn0  47445  prpair  47463  prproropf1olem0  47464  clnbgrel  47790  clnbgrsym  47799  2zrngnmrid  48179  rrx2linest  48670  pm5.32dav  48721  resinsnALT  48796  thincsect2  49302  lmdfval  49471  cmdfval  49472