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  1864  19.42v  1957  19.42  2229  sbel2x  2474  eu6  2574  moanmo  2624  2eu3  2655  2eu7  2659  2eu8  2660  eq2tri  2805  r19.42v  3278  rexcomf  3283  rabswap  3422  spc2ed  3539  euxfr2w  3656  euxfr2  3658  rmo4  3666  reu8  3669  rmo3f  3670  reuxfrd  3684  rmo3  3823  incomOLD  4137  difin2  4227  rcompleq  4231  euelss  4257  ssunsn  4763  uniprg  4858  inuni  5269  eqvinop  5403  elxp2  5615  elvvv  5664  brinxp2  5666  dmuni  5825  imadmrn  5981  asymref2  6024  cnvxp  6062  xpdifid  6073  cnvcnvsn  6124  opswap  6134  mptpreima  6143  xpco  6194  dfpo2  6201  fncnv  6509  fnres  6561  mptfnf  6570  dff1o2  6723  f13dfv  7148  fliftcnv  7184  isoini  7211  elrnmpores  7411  ndmovcom  7459  uniuni  7612  opabex3rd  7809  mptmpoopabbrd  7921  fsplit  7955  brtpos  8049  tposmpo  8077  oaord  8376  nnaord  8448  pmex  8618  mapsnend  8824  snmapen  8826  xpsnen  8840  xpcomco  8847  elfi2  9171  supmo  9209  infmo  9252  frind  9506  cp  9647  dfac5lem1  9877  dfac5lem2  9878  dfac2b  9884  kmlem3  9906  cflim3  10016  brdom7disj  10285  brdom6disj  10286  recmulnq  10718  lesub0  11490  wloglei  11505  creur  11965  indstr  12654  xmulcom  12998  xmulneg1  13001  xmulf  13004  iccneg  13202  fzrev  13317  injresinj  13506  rediv  14840  imdiv  14847  lenegsq  15030  o1lo1  15244  fsumcom2  15484  fsumcom  15485  fprodcom2  15692  fprodcom  15693  divalglem10  16109  smueqlem  16195  gcdcom  16218  lcmcom  16296  isprm2  16385  isprm7  16411  infpn2  16612  imasleval  17250  dfiso3  17483  posglbmo  18128  odulatb  18150  oduclatb  18223  oppgid  18961  gsumcom  19576  gsumcom3  19577  dfrhm2  19959  xrsdsreclb  20643  opsrtoslem1  21260  madutpos  21789  fvmptnn04if  21996  ntreq0  22226  ist0-3  22494  txkgen  22801  trfil2  23036  flimrest  23132  blres  23582  metrest  23678  restmetu  23724  elii1  24096  isclmp  24258  evthicc2  24622  ovolfcl  24628  dyaddisj  24758  iblpos  24955  itgposval  24958  ditgsplit  25023  itgsubst  25211  sincosq3sgn  25655  cos11  25687  dvdsflsumcom  26335  fsumvma  26359  logfaclbnd  26368  dchrelbas3  26384  lgsdi  26480  lgsquadlem3  26528  2lgslem1a  26537  istrkg2ld  26819  tgjustf  26832  tgcgr4  26890  mirreu3  27013  hpgcom  27126  colhp  27129  dfcgra2  27189  nbgrel  27705  nbgrsym  27728  wlkson  28022  isspthonpth  28114  usgr2pth0  28130  wwlksnextinj  28261  elwspths2spth  28329  rusgrnumwwlkl1  28330  clwwlknclwwlkdifnum  28341  clwwlkn1  28402  clwwlkn2  28405  iseupthf1o  28563  eupth2lem2  28580  frgrncvvdeqlem2  28661  fusgr2wsp2nb  28695  fusgreg2wsp  28697  frgrreg  28755  frgrregord013  28756  h2hcau  29338  nmopub  30267  nmfnleub  30284  chrelati  30723  cvexchlem  30727  mdsymlem8  30769  sumdmdii  30774  nelbOLDOLD  30814  2reucom  30825  reuxfrdf  30836  dmrab  30841  difrab2  30842  ressupprn  31021  2ndpreima  31037  fpwrelmapffslem  31064  xrofsup  31087  mgccnv  31274  pmtrprfv2  31354  smatrcl  31743  cnvordtrestixx  31860  issgon  32088  eulerpartlemr  32338  eulerpartlemgvv  32340  ballotlem2  32452  sgn3da  32505  oddprm2  32632  bnj257  32683  bnj545  32872  bnj594  32889  satfv0  33317  satfvsuclem1  33318  dfdm5  33744  dfrn5  33745  elima4  33747  sletri3  33955  nocvxmin  33970  sltrec  34011  elfix  34202  dffix2  34204  brimg  34236  brsuccf  34240  dfrecs2  34249  dfrdg4  34250  cgrcomlr  34297  ofscom  34306  btwnexch  34324  fscgr  34379  bj-df-ifc  34758  bj-dfmpoa  35286  bj-eldiag  35344  bj-imdirco  35358  bj-ccinftydisj  35381  mptsnunlem  35506  topdifinffinlem  35515  fvineqsneq  35580  wl-cases2-dnf  35668  wl-ax11-lem4  35736  fin2solem  35760  poimirlem26  35800  poimirlem30  35804  poimirlem32  35806  ftc1anclem6  35852  ftc1anc  35855  heibor1  35965  isdrngo3  36114  isdmn3  36229  an2anr  36375  anan  36376  inxpxrn  36518  prtlem70  36868  lrelat  37025  islshpat  37028  atlrelat1  37332  ishlat2  37364  cdlemb3  38617  diblsmopel  39182  dicelval3  39191  diclspsn  39205  uzindd  39982  3factsumint2  40027  3factsumint3  40028  3factsumint  40030  fz1eqin  40588  diophrex  40594  fphpd  40635  fzneg  40801  expdioph  40842  dford4  40848  lnr2i  40938  fgraphopab  41032  ifpancor  41050  ifpidg  41077  ifpid2g  41079  ifpid1g  41080  ifpim23g  41081  rp-fakeoranass  41100  dfid7  41190  dfrtrcl5  41207  relexp0eq  41279  fsovrfovd  41587  rr-grothprimbi  41883  uunT1p1  42371  uun132p1  42376  un2122  42380  uun2131p1  42382  uunT12p1  42390  uunT12p2  42391  uunT12p3  42392  uun2221  42403  uun2221p1  42404  uun2221p2  42405  3impdirp1  42406  ancomstVD  42455  icccncfext  43398  dvnmul  43454  dvmptfprodlem  43455  dvnprodlem2  43458  fourierdlem42  43660  fourierdlem83  43700  f1cof1b  44536  2reu3  44569  2reu7  44570  2reu8  44571  2reuimp0  44573  ndmaovcom  44664  an4com24  44727  4an21  44729  sprvalpwn0  44902  prpair  44920  prproropf1olem0  44921  2zrngnmrid  45475  opeliun2xp  45635  rrx2linest  46055  pm5.32dav  46106  iscnrm3lem3  46196  thincsect2  46306