Theorem ancom 464

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

Syntax hints:   ↔ wb 209   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  ancomd  465  biancomi  466  biancomd  467  ancomst  468  pm4.71r  562  pm5.32ri  579  pm5.32rd  581  bianassc  642  an12  644  an13  646  an42  656  andir  1006  cases2  1043  dfifp6  1064  ifpn  1069  excxor  1508  cador  1610  cadcoma  1614  exancom  1862  19.42v  1954  19.42  2236  sbel2x  2487  eu6  2634  moanmo  2684  2eu3  2715  2eu7  2720  2eu8  2721  eq2tri  2860  r19.42v  3303  rexcomOLD  3309  rexcomf  3311  rabswap  3436  spc2ed  3550  euxfr2w  3659  euxfr2  3661  rmo4  3669  reu8  3672  rmo3f  3673  reuxfrd  3687  rmo3  3818  incomOLD  4129  difin2  4216  rcompleq  4220  euelss  4242  ssunsn  4721  inuni  5210  eqvinop  5343  elxp2  5543  elvvv  5591  brinxp2  5593  dmuni  5747  imadmrn  5906  asymref2  5944  cnvxp  5981  xpdifid  5992  cnvcnvsn  6043  opswap  6053  mptpreima  6059  xpco  6108  fncnv  6397  fnres  6446  mptfnf  6455  dff1o2  6595  f13dfv  7009  fliftcnv  7043  isoini  7070  elrnmpores  7267  ndmovcom  7315  uniuni  7464  opabex3rd  7649  mptmpoopabbrd  7761  fsplit  7795  brtpos  7884  tposmpo  7912  oaord  8156  nnaord  8228  pmex  8394  mapsnend  8571  snmapen  8573  xpsnen  8584  xpcomco  8590  elfi2  8862  supmo  8900  infmo  8943  cp  9304  dfac5lem1  9534  dfac5lem2  9535  dfac2b  9541  kmlem3  9563  cflim3  9673  brdom7disj  9942  brdom6disj  9943  recmulnq  10375  lesub0  11146  wloglei  11161  creur  11619  indstr  12304  xmulcom  12647  xmulneg1  12650  xmulf  12653  iccneg  12850  fzrev  12965  injresinj  13153  rediv  14482  imdiv  14489  lenegsq  14672  o1lo1  14886  fsumcom2  15121  fsumcom  15122  fprodcom2  15330  fprodcom  15331  divalglem10  15743  smueqlem  15829  gcdcom  15852  lcmcom  15927  isprm2  16016  isprm7  16042  infpn2  16239  imasleval  16806  dfiso3  17035  odulatb  17745  oduclatb  17746  posglbmo  17749  oppgid  18476  gsumcom  19090  gsumcom3  19091  dfrhm2  19465  xrsdsreclb  20138  opsrtoslem1  20723  madutpos  21247  fvmptnn04if  21454  ntreq0  21682  ist0-3  21950  txkgen  22257  trfil2  22492  flimrest  22588  blres  23038  metrest  23131  restmetu  23177  elii1  23540  isclmp  23702  evthicc2  24064  ovolfcl  24070  dyaddisj  24200  iblpos  24396  itgposval  24399  ditgsplit  24464  itgsubst  24652  sincosq3sgn  25093  cos11  25125  dvdsflsumcom  25773  fsumvma  25797  logfaclbnd  25806  dchrelbas3  25822  lgsdi  25918  lgsquadlem3  25966  2lgslem1a  25975  istrkg2ld  26254  tgjustf  26267  tgcgr4  26325  mirreu3  26448  hpgcom  26561  colhp  26564  dfcgra2  26624  nbgrel  27130  nbgrsym  27153  wlkson  27446  isspthonpth  27538  usgr2pth0  27554  wwlksnextinj  27685  elwspths2spth  27753  rusgrnumwwlkl1  27754  clwwlknclwwlkdifnum  27765  clwwlkn1  27826  clwwlkn2  27829  iseupthf1o  27987  eupth2lem2  28004  frgrncvvdeqlem2  28085  fusgr2wsp2nb  28119  fusgreg2wsp  28121  frgrreg  28179  frgrregord013  28180  h2hcau  28762  nmopub  29691  nmfnleub  29708  chrelati  30147  cvexchlem  30151  mdsymlem8  30193  sumdmdii  30198  nelbOLD  30239  2reucom  30250  reuxfrdf  30262  dmrab  30267  difrab2  30268  ressupprn  30450  2ndpreima  30467  fpwrelmapffslem  30494  xrofsup  30518  mcgcnv  30705  pmtrprfv2  30782  smatrcl  31149  cnvordtrestixx  31266  issgon  31492  eulerpartlemr  31742  eulerpartlemgvv  31744  ballotlem2  31856  sgn3da  31909  oddprm2  32036  bnj257  32087  bnj545  32277  bnj594  32294  satfv0  32718  satfvsuclem1  32719  dfpo2  33104  dfdm5  33129  dfrn5  33130  elima4  33132  frind  33198  sletri3  33347  nocvxmin  33361  sltrec  33391  elfix  33477  dffix2  33479  brimg  33511  brsuccf  33515  dfrecs2  33524  dfrdg4  33525  cgrcomlr  33572  ofscom  33581  btwnexch  33599  fscgr  33654  bj-df-ifc  34026  bj-dfmpoa  34533  bj-eldiag  34591  bj-imdirco  34605  bj-ccinftydisj  34628  mptsnunlem  34755  topdifinffinlem  34764  fvineqsneq  34829  wl-cases2-dnf  34917  wl-ax11-lem4  34985  fin2solem  35043  poimirlem4  35061  poimirlem26  35083  poimirlem30  35087  poimirlem32  35089  ftc1anclem6  35135  ftc1anc  35138  heibor1  35248  isdrngo3  35397  isdmn3  35512  an2anr  35658  anan  35659  inxpxrn  35803  prtlem70  36153  lrelat  36310  islshpat  36313  atlrelat1  36617  ishlat2  36649  cdlemb3  37902  diblsmopel  38467  dicelval3  38476  diclspsn  38490  uzindd  39264  3factsumint2  39310  3factsumint3  39311  3factsumint  39313  fz1eqin  39710  diophrex  39716  fphpd  39757  fzneg  39923  expdioph  39964  dford4  39970  lnr2i  40060  fgraphopab  40154  ifpancor  40172  ifpidg  40199  ifpid2g  40201  ifpid1g  40202  ifpim23g  40203  rp-fakeoranass  40222  dfid7  40312  dfrtrcl5  40329  relexp0eq  40402  fsovrfovd  40710  rr-grothprimbi  41003  uunT1p1  41487  uun132p1  41492  un2122  41496  uun2131p1  41498  uunT12p1  41506  uunT12p2  41507  uunT12p3  41508  uun2221  41519  uun2221p1  41520  uun2221p2  41521  3impdirp1  41522  ancomstVD  41571  icccncfext  42529  dvnmul  42585  dvmptfprodlem  42586  dvnprodlem2  42589  fourierdlem42  42791  fourierdlem83  42831  2reu3  43666  2reu7  43667  2reu8  43668  2reuimp0  43670  ndmaovcom  43761  an4com24  43824  4an21  43826  sprvalpwn0  44000  prpair  44018  prproropf1olem0  44019  2zrngnmrid  44574  opeliun2xp  44734  rrx2linest  45156