Theorem ancom 461

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

Syntax hints:   ↔ wb 205   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  ancomd  462  biancomi  463  biancomd  464  ancomst  465  pm4.71r  559  pm5.32ri  576  pm5.32rd  578  bianassc  640  an12  642  an13  644  an42  654  andir  1006  cases2  1045  dfifp6  1066  ifpn  1071  excxor  1512  cador  1610  cadcoma  1614  exancom  1865  19.42v  1958  19.42  2230  sbel2x  2475  eu6  2575  moanmo  2625  2eu3  2656  2eu7  2660  2eu8  2661  eq2tri  2806  r19.42v  3280  rexcomf  3285  rabswap  3424  spc2ed  3541  euxfr2w  3656  euxfr2  3658  rmo4  3666  reu8  3669  rmo3f  3670  reuxfrd  3684  rmo3  3823  difin2  4226  rcompleq  4230  euelss  4256  ssunsn  4762  uniprg  4857  inuni  5268  eqvinop  5402  elxp2  5614  elvvv  5663  brinxp2  5665  dmuni  5826  imadmrn  5982  asymref2  6027  cnvxp  6065  xpdifid  6076  cnvcnvsn  6127  opswap  6137  mptpreima  6146  xpco  6196  dfpo2  6203  fncnv  6514  fnres  6568  mptfnf  6577  dff1o2  6730  f13dfv  7155  fliftcnv  7191  isoini  7218  elrnmpores  7420  ndmovcom  7468  uniuni  7621  opabex3rd  7818  mptmpoopabbrd  7930  mptmpoopabbrdOLD  7932  fsplit  7966  brtpos  8060  tposmpo  8088  oaord  8387  nnaord  8459  pmex  8629  mapsnend  8835  snmapen  8837  xpsnen  8851  xpcomco  8858  elfi2  9182  supmo  9220  infmo  9263  frind  9517  cp  9658  dfac5lem1  9888  dfac5lem2  9889  dfac2b  9895  kmlem3  9917  cflim3  10027  brdom7disj  10296  brdom6disj  10297  recmulnq  10729  lesub0  11501  wloglei  11516  creur  11976  indstr  12665  xmulcom  13009  xmulneg1  13012  xmulf  13015  iccneg  13213  fzrev  13328  injresinj  13517  rediv  14851  imdiv  14858  lenegsq  15041  o1lo1  15255  fsumcom2  15495  fsumcom  15496  fprodcom2  15703  fprodcom  15704  divalglem10  16120  smueqlem  16206  gcdcom  16229  lcmcom  16307  isprm2  16396  isprm7  16422  infpn2  16623  imasleval  17261  dfiso3  17494  posglbmo  18139  odulatb  18161  oduclatb  18234  oppgid  18972  gsumcom  19587  gsumcom3  19588  dfrhm2  19970  xrsdsreclb  20654  opsrtoslem1  21271  madutpos  21800  fvmptnn04if  22007  ntreq0  22237  ist0-3  22505  txkgen  22812  trfil2  23047  flimrest  23143  blres  23593  metrest  23689  restmetu  23735  elii1  24107  isclmp  24269  evthicc2  24633  ovolfcl  24639  dyaddisj  24769  iblpos  24966  itgposval  24969  ditgsplit  25034  itgsubst  25222  sincosq3sgn  25666  cos11  25698  dvdsflsumcom  26346  fsumvma  26370  logfaclbnd  26379  dchrelbas3  26395  lgsdi  26491  lgsquadlem3  26539  2lgslem1a  26548  istrkg2ld  26830  tgjustf  26843  tgcgr4  26901  mirreu3  27024  hpgcom  27137  colhp  27140  dfcgra2  27200  nbgrel  27716  nbgrsym  27739  wlkson  28033  isspthonpth  28126  usgr2pth0  28142  wwlksnextinj  28273  elwspths2spth  28341  rusgrnumwwlkl1  28342  clwwlknclwwlkdifnum  28353  clwwlkn1  28414  clwwlkn2  28417  iseupthf1o  28575  eupth2lem2  28592  frgrncvvdeqlem2  28673  fusgr2wsp2nb  28707  fusgreg2wsp  28709  frgrreg  28767  frgrregord013  28768  h2hcau  29350  nmopub  30279  nmfnleub  30296  chrelati  30735  cvexchlem  30739  mdsymlem8  30781  sumdmdii  30786  nelbOLDOLD  30826  2reucom  30837  reuxfrdf  30848  dmrab  30853  difrab2  30854  ressupprn  31033  2ndpreima  31049  fpwrelmapffslem  31076  xrofsup  31099  mgccnv  31286  pmtrprfv2  31366  smatrcl  31755  cnvordtrestixx  31872  issgon  32100  eulerpartlemr  32350  eulerpartlemgvv  32352  ballotlem2  32464  sgn3da  32517  oddprm2  32644  bnj257  32695  bnj545  32884  bnj594  32901  satfv0  33329  satfvsuclem1  33330  dfdm5  33756  dfrn5  33757  elima4  33759  sletri3  33967  nocvxmin  33982  sltrec  34023  elfix  34214  dffix2  34216  brimg  34248  brsuccf  34252  dfrecs2  34261  dfrdg4  34262  cgrcomlr  34309  ofscom  34318  btwnexch  34336  fscgr  34391  bj-df-ifc  34770  bj-dfmpoa  35298  bj-eldiag  35356  bj-imdirco  35370  bj-ccinftydisj  35393  mptsnunlem  35518  topdifinffinlem  35527  fvineqsneq  35592  wl-cases2-dnf  35680  wl-ax11-lem4  35748  fin2solem  35772  poimirlem26  35812  poimirlem30  35816  poimirlem32  35818  ftc1anclem6  35864  ftc1anc  35867  heibor1  35977  isdrngo3  36126  isdmn3  36241  an2anr  36387  anan  36388  inxpxrn  36528  prtlem70  36878  lrelat  37035  islshpat  37038  atlrelat1  37342  ishlat2  37374  cdlemb3  38627  diblsmopel  39192  dicelval3  39201  diclspsn  39215  uzindd  39992  3factsumint2  40037  3factsumint3  40038  3factsumint  40040  fz1eqin  40598  diophrex  40604  fphpd  40645  fzneg  40811  expdioph  40852  dford4  40858  lnr2i  40948  fgraphopab  41042  ifpancor  41078  ifpidg  41105  ifpid2g  41107  ifpid1g  41108  ifpim23g  41109  rp-fakeoranass  41128  minregex  41148  dfid7  41227  dfrtrcl5  41244  relexp0eq  41316  fsovrfovd  41624  rr-grothprimbi  41920  uunT1p1  42408  uun132p1  42413  un2122  42417  uun2131p1  42419  uunT12p1  42427  uunT12p2  42428  uunT12p3  42429  uun2221  42440  uun2221p1  42441  uun2221p2  42442  3impdirp1  42443  ancomstVD  42492  icccncfext  43435  dvnmul  43491  dvmptfprodlem  43492  dvnprodlem2  43495  fourierdlem42  43697  fourierdlem83  43737  f1cof1b  44580  2reu3  44613  2reu7  44614  2reu8  44615  2reuimp0  44617  ndmaovcom  44708  an4com24  44771  4an21  44773  sprvalpwn0  44946  prpair  44964  prproropf1olem0  44965  2zrngnmrid  45519  opeliun2xp  45679  rrx2linest  46099  pm5.32dav  46150  iscnrm3lem3  46240  thincsect2  46350