Theorem ancom 460

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

Syntax hints:   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  ancomd  461  biancomi  462  biancomd  463  ancomst  464  pm4.71r  558  pm5.32ri  575  pm5.32rd  578  an2anr  636  bianassc  643  an12  645  an13  647  an42  657  andir  1010  cases2  1047  dfifp6  1068  ifpn  1073  4anpull2  1362  excxor  1517  cador  1609  cadcoma  1613  exancom  1862  19.42v  1954  19.42  2239  sbel2x  2474  eu6  2569  moanmo  2617  2eu3  2649  2eu7  2653  2eu8  2654  eq2tri  2793  r19.42v  3164  rexcomf  3271  rabswap  3404  spc2ed  3551  euxfr2w  3674  euxfr2  3676  rmo4  3684  reu8  3687  rmo3f  3688  reuxfrd  3702  rmo3  3835  difin2  4246  rcompleq  4250  euelss  4277  ssunsn  4775  uniprg  4870  inuni  5283  eqvinop  5422  elxp2  5635  opeliun2xp  5679  elvvv  5687  brinxp2  5689  dmuni  5849  imadmrn  6014  asymref2  6059  cnvopab  6079  cnvxp  6099  xpdifid  6110  cnvcnvsn  6161  opswap  6171  mptpreima  6180  xpco  6231  dfpo2  6238  fncnv  6549  fnres  6603  mptfnf  6611  dff1o2  6763  f13dfv  7203  fliftcnv  7240  isoini  7267  elrnmpores  7479  ndmovcom  7528  uniuni  7690  opabex3rd  7893  mptmpoopabbrd  8007  mptmpoopabbrdOLD  8008  fsplit  8042  brtpos  8160  tposmpo  8188  oaord  8457  nnaord  8529  naddasslem1  8604  naddasslem2  8605  brinxper  8646  pmex  8750  mapsnend  8953  snmapen  8955  xpsnen  8969  xpcomco  8975  elfi2  9293  supmo  9331  infmo  9376  frind  9638  cp  9779  dfac5lem1  10009  dfac5lem2  10010  dfac2b  10017  kmlem3  10039  cflim3  10148  brdom7disj  10417  brdom6disj  10418  recmulnq  10850  lesub0  11629  wloglei  11644  creur  12114  indstr  12809  xmulcom  13160  xmulneg1  13163  xmulf  13166  iccneg  13367  fzrev  13482  injresinj  13686  rediv  15033  imdiv  15040  lenegsq  15223  o1lo1  15439  fsumcom2  15676  fsumcom  15677  fprodcom2  15886  fprodcom  15887  divalglem10  16308  smueqlem  16396  gcdcom  16419  lcmcom  16499  isprm2  16588  isprm7  16614  infpn2  16820  imasleval  17440  dfiso3  17675  posglbmo  18311  odulatb  18335  oduclatb  18408  oppgid  19263  gsumcom  19884  gsumcom3  19885  dfrhm2  20387  xrsdsreclb  21345  opsrtoslem1  21985  psdmvr  22079  madutpos  22552  fvmptnn04if  22759  ntreq0  22987  ist0-3  23255  txkgen  23562  trfil2  23797  flimrest  23893  blres  24341  metrest  24434  restmetu  24480  elii1  24853  isclmp  25019  evthicc2  25383  ovolfcl  25389  dyaddisj  25519  iblpos  25716  itgposval  25719  ditgsplit  25784  itgsubst  25978  sincosq3sgn  26431  cos11  26464  dvdsflsumcom  27120  fsumvma  27146  logfaclbnd  27155  dchrelbas3  27171  lgsdi  27267  lgsquadlem3  27315  2lgslem1a  27324  sletri3  27689  sltrec  27757  istrkg2ld  28433  tgjustf  28446  tgcgr4  28504  mirreu3  28627  hpgcom  28740  colhp  28743  dfcgra2  28803  nbgrel  29313  nbgrsym  29336  wlkson  29628  dfpth2  29702  isspthonpth  29722  usgr2pth0  29738  wwlksnextinj  29872  elwspths2spth  29940  rusgrnumwwlkl1  29941  clwwlknclwwlkdifnum  29952  clwwlkn1  30013  clwwlkn2  30016  iseupthf1o  30174  eupth2lem2  30191  frgrncvvdeqlem2  30272  fusgr2wsp2nb  30306  fusgreg2wsp  30308  frgrreg  30366  frgrregord013  30367  h2hcau  30951  nmopub  31880  nmfnleub  31897  chrelati  32336  cvexchlem  32340  mdsymlem8  32382  sumdmdii  32387  13an22anass  32435  2reucom  32451  reuxfrdf  32462  dmrab  32468  difrab2  32469  ressupprn  32663  2ndpreima  32681  fpwrelmapffslem  32707  xrofsup  32742  sgn3da  32809  mgccnv  32972  pmtrprfv2  33049  smatrcl  33801  cnvordtrestixx  33918  issgon  34128  eulerpartlemr  34379  eulerpartlemgvv  34381  ballotlem2  34494  oddprm2  34660  bnj257  34711  bnj545  34899  bnj594  34916  nfan1c  35077  satfv0  35394  satfvsuclem1  35395  dfdm5  35809  dfrn5  35810  elima4  35812  elfix  35937  dffix2  35939  brimg  35971  brsuccf  35975  dfrecs2  35984  dfrdg4  35985  cgrcomlr  36032  ofscom  36041  btwnexch  36059  fscgr  36114  bj-df-ifc  36614  bj-dfmpoa  37152  bj-eldiag  37210  bj-imdirco  37224  bj-ccinftydisj  37247  mptsnunlem  37372  topdifinffinlem  37381  fvineqsneq  37446  wl-cases2-dnf  37546  wl-ax11-lem4  37622  fin2solem  37646  poimirlem26  37686  poimirlem30  37690  poimirlem32  37692  ftc1anclem6  37738  ftc1anc  37741  heibor1  37850  isdrngo3  37999  isdmn3  38114  anan  38263  br1cnvinxp  38291  inxpxrn  38427  prtlem70  38896  lrelat  39053  islshpat  39056  atlrelat1  39360  ishlat2  39392  cdlemb3  40645  diblsmopel  41210  dicelval3  41219  diclspsn  41233  uzindd  42010  3factsumint2  42055  3factsumint3  42056  3factsumint  42058  fimgmcyc  42567  eu6w  42709  fz1eqin  42802  diophrex  42808  fphpd  42849  fzneg  43015  expdioph  43056  dford4  43062  lnr2i  43149  fgraphopab  43236  omge2  43331  oadif1lem  43412  oadif1  43413  ifpancor  43497  ifpidg  43524  ifpid2g  43526  ifpid1g  43527  ifpim23g  43528  rp-fakeoranass  43547  minregex  43567  dfid7  43645  dfrtrcl5  43662  relexp0eq  43734  fsovrfovd  44042  rr-grothprimbi  44328  uunT1p1  44813  uun132p1  44818  un2122  44822  uun2131p1  44824  uunT12p1  44832  uunT12p2  44833  uunT12p3  44834  uun2221  44845  uun2221p1  44846  uun2221p2  44847  3impdirp1  44848  ancomstVD  44897  icccncfext  45925  dvnmul  45981  dvmptfprodlem  45982  dvnprodlem2  45985  fourierdlem42  46187  fourierdlem83  46227  f1cof1b  47108  2reu3  47141  2reu7  47142  2reu8  47143  2reuimp0  47145  ndmaovcom  47236  an4com24  47299  4an21  47301  sprvalpwn0  47514  prpair  47532  prproropf1olem0  47533  clnbgrel  47859  clnbgrsym  47869  2zrngnmrid  48287  rrx2linest  48774  pm5.32dav  48825  resinsnALT  48904  catcinv  49431  thincsect2  49500  lmdfval  49681  cmdfval  49682