Theorem ancom 462

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

Syntax hints:   ↔ wb 208   ∧ wa 397

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 209  df-an 398

This theorem is referenced by:  ancomd  463  biancomi  464  biancomd  465  ancomst  466  pm4.71r  564  pm5.32ri  581  pm5.32rd  584  an2anr  643  bianassc  650  an12  652  an13  654  an42  664  andir  1017  cases2  1054  dfifp6  1075  ifpn  1080  4anpull2  1369  excxor  1524  cador  1616  cadcoma  1620  exancom  1869  19.42v  1961  19.42  2250  sbel2x  2484  eu6  2580  moanmo  2628  2eu3  2659  2eu7  2663  2eu8  2664  eq2tri  2803  r19.42v  3173  rexcomf  3280  rabswap  3402  spc2ed  3540  euxfr2w  3662  euxfr2  3664  rmo4  3672  reu8  3675  rmo3f  3676  reuxfrd  3690  rmo3  3822  difin2  4231  rcompleq  4235  euelss  4262  ssunsn  4761  uniprg  4856  inuni  5280  eqvinop  5429  elxp2  5644  opeliun2xp  5688  elvvv  5696  brinxp2  5698  dmuni  5862  imadmrn  6028  asymref2  6073  cnvopab  6093  cnvxp  6111  xpdifid  6122  cnvcnvsn  6173  opswap  6183  mptpreima  6192  xpco  6243  dfpo2  6250  fncnv  6561  fnres  6615  mptfnf  6623  dff1o2  6775  f13dfv  7221  fliftcnv  7258  isoini  7285  elrnmpores  7497  ndmovcom  7546  uniuni  7708  opabex3rd  7910  mptmpoopabbrd  8024  fsplit  8058  brtpos  8177  tposmpo  8205  oaord  8476  nnaord  8549  naddasslem1  8624  naddasslem2  8625  brinxper  8667  pmex  8772  mapsnend  8977  snmapen  8979  xpsnen  8993  xpcomco  8999  elfi2  9321  supmo  9359  infmo  9404  frind  9669  cp  9810  dfac5lem1  10040  dfac5lem2  10041  dfac2b  10048  kmlem3  10070  cflim3  10180  brdom7disj  10449  brdom6disj  10450  recmulnq  10883  lesub0  11663  wloglei  11678  creur  12148  indstr  12861  xmulcom  13213  xmulneg1  13216  xmulf  13219  iccneg  13420  fzrev  13536  injresinj  13741  rediv  15088  imdiv  15095  lenegsq  15278  o1lo1  15494  fsumcom2  15731  fsumcom  15732  fprodcom2  15944  fprodcom  15945  divalglem10  16366  smueqlem  16454  gcdcom  16477  lcmcom  16557  isprm2  16646  isprm7  16673  infpn2  16879  imasleval  17500  dfiso3  17735  posglbmo  18371  odulatb  18395  oduclatb  18468  oppgid  19325  gsumcom  19946  gsumcom3  19947  dfrhm2  20448  xrsdsreclb  21392  opsrtoslem1  22034  psdmvr  22160  madutpos  22628  fvmptnn04if  22835  ntreq0  23063  ist0-3  23331  txkgen  23638  trfil2  23873  flimrest  23969  blres  24417  metrest  24510  restmetu  24556  elii1  24923  isclmp  25085  evthicc2  25448  ovolfcl  25454  dyaddisj  25584  iblpos  25781  itgposval  25784  ditgsplit  25849  itgsubst  26037  sincosq3sgn  26485  cos11  26518  dvdsflsumcom  27172  fsumvma  27197  logfaclbnd  27206  dchrelbas3  27222  lgsdi  27318  lgsquadlem3  27366  2lgslem1a  27375  lestri3  27739  ltsrec  27813  istrkg2ld  28548  tgjustf  28561  tgcgr4  28619  mirreu3  28742  hpgcom  28855  colhp  28858  dfcgra2  28918  nbgrel  29429  nbgrsym  29452  wlkson  29743  dfpth2  29817  isspthonpth  29837  usgr2pth0  29853  wwlksnextinj  29987  elwspths2spth  30058  rusgrnumwwlkl1  30059  clwwlknclwwlkdifnum  30070  clwwlkn1  30131  clwwlkn2  30134  iseupthf1o  30292  eupth2lem2  30309  frgrncvvdeqlem2  30390  fusgr2wsp2nb  30424  fusgreg2wsp  30426  frgrreg  30484  frgrregord013  30485  h2hcau  31070  nmopub  31999  nmfnleub  32016  chrelati  32455  cvexchlem  32459  mdsymlem8  32501  sumdmdii  32506  13an22anass  32553  2reucom  32569  reuxfrdf  32580  dmrab  32586  difrab2  32587  ififcom  32640  ressupprn  32784  2ndpreima  32802  fpwrelmapffslem  32826  xrofsup  32861  sgn3da  32928  mgccnv  33080  pmtrprfv2  33171  smatrcl  33990  cnvordtrestixx  34107  issgon  34317  eulerpartlemr  34568  eulerpartlemgvv  34570  ballotlem2  34683  oddprm2  34849  bnj257  34903  bnj545  35090  bnj594  35107  nfan1c  35268  satfv0  35599  satfvsuclem1  35600  dfdm5  36014  dfrn5  36015  elima4  36017  elfix  36142  dffix2  36144  brimg  36176  lemsuccf  36180  dfrecs2  36191  dfrdg4  36192  cgrcomlr  36239  ofscom  36248  btwnexch  36266  fscgr  36321  bj-df-ifc  36904  bj-axseprep  37440  bj-dfmpoa  37489  bj-eldiag  37549  bj-imdirco  37563  bj-ccinftydisj  37586  mptsnunlem  37713  topdifinffinlem  37722  fvineqsneq  37787  wl-cases2-dnf  37896  fin2solem  37986  poimirlem26  38026  poimirlem30  38030  poimirlem32  38032  ftc1anclem6  38078  ftc1anc  38081  heibor1  38190  isdrngo3  38339  isdmn3  38454  anan  38615  br1cnvinxp  38639  raldmqseu  38745  inxpxrn  38798  prtlem70  39362  lrelat  39519  islshpat  39522  atlrelat1  39826  ishlat2  39858  cdlemb3  41111  diblsmopel  41676  dicelval3  41685  diclspsn  41699  uzindd  42476  3factsumint2  42520  3factsumint3  42521  3factsumint  42523  fimgmcyc  43033  eu6w  43139  fz1eqin  43231  diophrex  43237  fphpd  43274  fzneg  43440  expdioph  43481  dford4  43487  lnr2i  43574  fgraphopab  43661  omge2  43756  oadif1lem  43837  oadif1  43838  ifpancor  43921  ifpidg  43948  ifpid2g  43950  ifpid1g  43951  ifpim23g  43952  rp-fakeoranass  43971  minregex  43991  dfid7  44069  dfrtrcl5  44086  relexp0eq  44158  fsovrfovd  44466  rr-grothprimbi  44752  uunT1p1  45237  uun132p1  45242  un2122  45246  uun2131p1  45248  uunT12p1  45256  uunT12p2  45257  uunT12p3  45258  uun2221  45269  uun2221p1  45270  uun2221p2  45271  3impdirp1  45272  ancomstVD  45321  icccncfext  46342  dvnmul  46398  dvmptfprodlem  46399  dvnprodlem2  46402  fourierdlem42  46604  fourierdlem83  46644  f1cof1b  47552  2reu3  47585  2reu7  47586  2reu8  47587  2reuimp0  47589  ndmaovcom  47680  an4com24  47743  4an21  47745  sprvalpwn0  47970  prpair  47988  prproropf1olem0  47989  clnbgrel  48331  clnbgrsym  48341  2zrngnmrid  48759  rrx2linest  49245  pm5.32dav  49296  resinsnALT  49375  catcinv  49901  thincsect2  49970  lmdfval  50151  cmdfval  50152