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 208	1 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜓 ∧ 𝜑))

Syntax hints:   ↔ wb 205   ∧ 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 206  df-an 398

This theorem is referenced by:  ancomd  463  biancomi  464  biancomd  465  ancomst  466  pm4.71r  560  pm5.32ri  577  pm5.32rd  579  an2anr  636  bianassc  642  an12  644  an13  646  an42  656  andir  1008  cases2  1047  dfifp6  1068  ifpn  1073  excxor  1516  cador  1610  cadcoma  1614  exancom  1865  19.42v  1958  19.42  2230  sbel2x  2474  eu6  2569  moanmo  2619  2eu3  2650  2eu7  2654  2eu8  2655  eq2tri  2800  r19.42v  3191  rexcomf  3301  rabswap  3442  spc2ed  3592  euxfr2w  3717  euxfr2  3719  rmo4  3727  reu8  3730  rmo3f  3731  reuxfrd  3745  rmo3  3884  difin2  4292  rcompleq  4296  euelss  4322  ssunsn  4832  uniprg  4926  inuni  5344  eqvinop  5488  elxp2  5701  elvvv  5752  brinxp2  5754  dmuni  5915  imadmrn  6070  asymref2  6119  cnvxp  6157  xpdifid  6168  cnvcnvsn  6219  opswap  6229  mptpreima  6238  xpco  6289  dfpo2  6296  fncnv  6622  fnres  6678  mptfnf  6686  dff1o2  6839  f13dfv  7272  fliftcnv  7308  isoini  7335  elrnmpores  7546  ndmovcom  7594  uniuni  7749  opabex3rd  7953  mptmpoopabbrd  8067  mptmpoopabbrdOLD  8069  fsplit  8103  brtpos  8220  tposmpo  8248  oaord  8547  nnaord  8619  naddasslem1  8693  naddasslem2  8694  pmex  8825  mapsnend  9036  snmapen  9038  xpsnen  9055  xpcomco  9062  elfi2  9409  supmo  9447  infmo  9490  frind  9745  cp  9886  dfac5lem1  10118  dfac5lem2  10119  dfac2b  10125  kmlem3  10147  cflim3  10257  brdom7disj  10526  brdom6disj  10527  recmulnq  10959  lesub0  11731  wloglei  11746  creur  12206  indstr  12900  xmulcom  13245  xmulneg1  13248  xmulf  13251  iccneg  13449  fzrev  13564  injresinj  13753  rediv  15078  imdiv  15085  lenegsq  15267  o1lo1  15481  fsumcom2  15720  fsumcom  15721  fprodcom2  15928  fprodcom  15929  divalglem10  16345  smueqlem  16431  gcdcom  16454  lcmcom  16530  isprm2  16619  isprm7  16645  infpn2  16846  imasleval  17487  dfiso3  17720  posglbmo  18365  odulatb  18387  oduclatb  18460  oppgid  19223  gsumcom  19845  gsumcom3  19846  dfrhm2  20253  xrsdsreclb  20992  opsrtoslem1  21616  madutpos  22144  fvmptnn04if  22351  ntreq0  22581  ist0-3  22849  txkgen  23156  trfil2  23391  flimrest  23487  blres  23937  metrest  24033  restmetu  24079  elii1  24451  isclmp  24613  evthicc2  24977  ovolfcl  24983  dyaddisj  25113  iblpos  25310  itgposval  25313  ditgsplit  25378  itgsubst  25566  sincosq3sgn  26010  cos11  26042  dvdsflsumcom  26692  fsumvma  26716  logfaclbnd  26725  dchrelbas3  26741  lgsdi  26837  lgsquadlem3  26885  2lgslem1a  26894  sletri3  27258  nocvxmin  27280  sltrec  27321  istrkg2ld  27711  tgjustf  27724  tgcgr4  27782  mirreu3  27905  hpgcom  28018  colhp  28021  dfcgra2  28081  nbgrel  28597  nbgrsym  28620  wlkson  28913  isspthonpth  29006  usgr2pth0  29022  wwlksnextinj  29153  elwspths2spth  29221  rusgrnumwwlkl1  29222  clwwlknclwwlkdifnum  29233  clwwlkn1  29294  clwwlkn2  29297  iseupthf1o  29455  eupth2lem2  29472  frgrncvvdeqlem2  29553  fusgr2wsp2nb  29587  fusgreg2wsp  29589  frgrreg  29647  frgrregord013  29648  h2hcau  30232  nmopub  31161  nmfnleub  31178  chrelati  31617  cvexchlem  31621  mdsymlem8  31663  sumdmdii  31668  13an22anass  31706  2reucom  31720  reuxfrdf  31731  dmrab  31737  difrab2  31738  ressupprn  31912  2ndpreima  31929  fpwrelmapffslem  31957  xrofsup  31980  mgccnv  32169  pmtrprfv2  32249  smatrcl  32776  cnvordtrestixx  32893  issgon  33121  eulerpartlemr  33373  eulerpartlemgvv  33375  ballotlem2  33487  sgn3da  33540  oddprm2  33667  bnj257  33718  bnj545  33906  bnj594  33923  satfv0  34349  satfvsuclem1  34350  dfdm5  34744  dfrn5  34745  elima4  34747  elfix  34875  dffix2  34877  brimg  34909  brsuccf  34913  dfrecs2  34922  dfrdg4  34923  cgrcomlr  34970  ofscom  34979  btwnexch  34997  fscgr  35052  bj-df-ifc  35457  bj-dfmpoa  35999  bj-eldiag  36057  bj-imdirco  36071  bj-ccinftydisj  36094  mptsnunlem  36219  topdifinffinlem  36228  fvineqsneq  36293  wl-cases2-dnf  36381  wl-ax11-lem4  36450  fin2solem  36474  poimirlem26  36514  poimirlem30  36518  poimirlem32  36520  ftc1anclem6  36566  ftc1anc  36569  heibor1  36678  isdrngo3  36827  isdmn3  36942  anan  37093  br1cnvinxp  37124  inxpxrn  37265  prtlem70  37727  lrelat  37884  islshpat  37887  atlrelat1  38191  ishlat2  38223  cdlemb3  39477  diblsmopel  40042  dicelval3  40051  diclspsn  40065  uzindd  40842  3factsumint2  40887  3factsumint3  40888  3factsumint  40890  fz1eqin  41507  diophrex  41513  fphpd  41554  fzneg  41721  expdioph  41762  dford4  41768  lnr2i  41858  fgraphopab  41952  omge2  42048  oadif1lem  42129  oadif1  42130  ifpancor  42215  ifpidg  42242  ifpid2g  42244  ifpid1g  42245  ifpim23g  42246  rp-fakeoranass  42265  minregex  42285  dfid7  42363  dfrtrcl5  42380  relexp0eq  42452  fsovrfovd  42760  rr-grothprimbi  43054  uunT1p1  43542  uun132p1  43547  un2122  43551  uun2131p1  43553  uunT12p1  43561  uunT12p2  43562  uunT12p3  43563  uun2221  43574  uun2221p1  43575  uun2221p2  43576  3impdirp1  43577  ancomstVD  43626  icccncfext  44603  dvnmul  44659  dvmptfprodlem  44660  dvnprodlem2  44663  fourierdlem42  44865  fourierdlem83  44905  f1cof1b  45785  2reu3  45818  2reu7  45819  2reu8  45820  2reuimp0  45822  ndmaovcom  45913  an4com24  45976  4an21  45978  sprvalpwn0  46151  prpair  46169  prproropf1olem0  46170  2zrngnmrid  46848  opeliun2xp  47008  rrx2linest  47428  pm5.32dav  47479  iscnrm3lem3  47568  thincsect2  47678