Theorem ancom 463

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

Syntax hints:   ↔ wb 208   ∧ wa 398

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 399

This theorem is referenced by:  ancomd  464  biancomi  465  biancomd  466  ancomst  467  pm4.71r  561  pm5.32ri  578  pm5.32rd  580  bianassc  641  an12  643  an13  645  an42  655  andir  1005  cases2  1042  dfifp6  1063  excxor  1505  cador  1605  cadcoma  1609  exancom  1857  19.42v  1950  19.42  2234  sbel2x  2494  eu6  2655  moanmo  2703  2eu3  2735  2eu3OLD  2736  2eu7  2741  2eu8  2742  eq2tri  2883  r19.28vOLD  3187  r19.29rOLD  3256  r19.42v  3350  rexcomOLD  3356  rexcomf  3358  rabswap  3488  spc2ed  3601  euxfr2w  3710  euxfr2  3712  rmo4  3720  reu8  3723  rmo3f  3724  reuxfrd  3738  rmo3  3871  rmo3OLD  3872  incomOLD  4178  difin2  4265  euelss  4289  ssunsn  4760  inuni  5245  eqvinop  5377  elxp2  5578  elvvv  5626  brinxp2  5628  dmuni  5782  imadmrn  5938  asymref2  5976  cnvxp  6013  xpdifid  6024  cnvcnvsn  6075  opswap  6085  mptpreima  6091  xpco  6139  fncnv  6426  fnres  6473  mptfnf  6482  dff1o2  6619  f13dfv  7030  fliftcnv  7063  isoini  7090  elrnmpores  7287  ndmovcom  7334  uniuni  7483  opabex3rd  7666  mptmpoopabbrd  7777  fsplit  7811  brtpos  7900  tposmpo  7928  oaord  8172  nnaord  8244  pmex  8410  mapsnend  8587  snmapen  8589  xpsnen  8600  xpcomco  8606  elfi2  8877  supmo  8915  infmo  8958  cp  9319  dfac5lem1  9548  dfac5lem2  9549  dfac2b  9555  kmlem3  9577  cflim3  9683  brdom7disj  9952  brdom6disj  9953  recmulnq  10385  lesub0  11156  wloglei  11171  creur  11631  indstr  12315  xmulcom  12658  xmulneg1  12661  xmulf  12664  iccneg  12857  fzrev  12969  injresinj  13157  rediv  14489  imdiv  14496  lenegsq  14679  o1lo1  14893  fsumcom2  15128  fsumcom  15129  fprodcom2  15337  fprodcom  15338  divalglem10  15752  smueqlem  15838  gcdcom  15861  lcmcom  15936  isprm2  16025  isprm7  16051  infpn2  16248  imasleval  16813  dfiso3  17042  odulatb  17752  oduclatb  17753  posglbmo  17756  oppgid  18483  gsumcom  19096  gsumcom3  19097  dfrhm2  19468  opsrtoslem1  20263  xrsdsreclb  20591  madutpos  21250  fvmptnn04if  21456  ntreq0  21684  ist0-3  21952  txkgen  22259  trfil2  22494  flimrest  22590  blres  23040  metrest  23133  restmetu  23179  elii1  23538  isclmp  23700  evthicc2  24060  ovolfcl  24066  dyaddisj  24196  iblpos  24392  itgposval  24395  ditgsplit  24458  itgsubst  24645  sincosq3sgn  25085  cos11  25116  dvdsflsumcom  25764  fsumvma  25788  logfaclbnd  25797  dchrelbas3  25813  lgsdi  25909  lgsquadlem3  25957  2lgslem1a  25966  istrkg2ld  26245  tgjustf  26258  tgcgr4  26316  mirreu3  26439  hpgcom  26552  colhp  26555  dfcgra2  26615  nbgrel  27121  nbgrsym  27144  wlkson  27437  isspthonpth  27529  usgr2pth0  27545  wwlksnextinj  27676  elwspths2spth  27745  rusgrnumwwlkl1  27746  clwwlknclwwlkdifnum  27757  clwwlkn1  27818  clwwlkn2  27821  iseupthf1o  27980  eupth2lem2  27997  frgrncvvdeqlem2  28078  fusgr2wsp2nb  28112  fusgreg2wsp  28114  frgrreg  28172  frgrregord013  28173  h2hcau  28755  nmopub  29684  nmfnleub  29701  chrelati  30140  cvexchlem  30144  mdsymlem8  30186  sumdmdii  30191  nelbOLD  30231  2reucom  30242  reuxfrdf  30254  dmrab  30259  difrab2  30260  2ndpreima  30442  fpwrelmapffslem  30467  xrofsup  30491  pmtrprfv2  30732  smatrcl  31061  cnvordtrestixx  31156  issgon  31382  eulerpartlemr  31632  eulerpartlemgvv  31634  ballotlem2  31746  sgn3da  31799  oddprm2  31926  bnj257  31977  bnj545  32167  bnj594  32184  satfv0  32605  satfvsuclem1  32606  dfpo2  32991  dfdm5  33016  dfrn5  33017  elima4  33019  frind  33085  sletri3  33234  nocvxmin  33248  sltrec  33278  elfix  33364  dffix2  33366  brimg  33398  brsuccf  33402  dfrecs2  33411  dfrdg4  33412  cgrcomlr  33459  ofscom  33468  btwnexch  33486  fscgr  33541  bj-df-ifc  33913  bj-dfmpoa  34409  bj-eldiag  34467  bj-ccinftydisj  34494  mptsnunlem  34618  topdifinffinlem  34627  fvineqsneq  34692  wl-cases2-dnf  34751  wl-ax11-lem4  34819  fin2solem  34877  poimirlem4  34895  poimirlem26  34917  poimirlem30  34921  poimirlem32  34923  ftc1anclem6  34971  ftc1anc  34974  heibor1  35087  isdrngo3  35236  isdmn3  35351  an2anr  35497  anan  35498  inxpxrn  35642  prtlem70  35992  lrelat  36149  islshpat  36152  atlrelat1  36456  ishlat2  36488  cdlemb3  37741  diblsmopel  38306  dicelval3  38315  diclspsn  38329  fz1eqin  39364  diophrex  39370  fphpd  39411  fzneg  39577  expdioph  39618  dford4  39624  lnr2i  39714  fgraphopab  39808  ifpancor  39827  ifpdfbi  39837  ifpidg  39855  ifpid2g  39857  ifpid1g  39858  ifpim23g  39859  rp-fakeoranass  39878  dfid7  39970  dfrtrcl5  39987  relexp0eq  40044  fsovrfovd  40353  rcompleq  40368  rr-grothprimbi  40629  uunT1p1  41113  uun132p1  41118  un2122  41122  uun2131p1  41124  uunT12p1  41132  uunT12p2  41133  uunT12p3  41134  uun2221  41145  uun2221p1  41146  uun2221p2  41147  3impdirp1  41148  ancomstVD  41197  icccncfext  42168  dvnmul  42226  dvmptfprodlem  42227  dvnprodlem2  42230  fourierdlem42  42433  fourierdlem83  42473  2reu3  43308  2reu7  43309  2reu8  43310  2reuimp0  43312  ndmaovcom  43403  an4com24  43466  4an21  43468  sprvalpwn0  43644  prpair  43662  prproropf1olem0  43663  2zrngnmrid  44220  opeliun2xp  44380  rrx2linest  44728