Theorem ancom 466

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  ancomd  467  biancomi  468  biancomd  469  ancomst  470  pm4.71r  568  pm5.32ri  586  pm5.32rd  589  an2anr  648  bianassc  656  an12  658  an13  660  an42  670  andir  1026  cases2  1063  dfifp6  1084  ifpn  1090  13an22anass  1379  4anpull2OLD  1383  excxor  1545  cador  1640  cadcoma  1644  exancom  1893  19.42v  1985  19.42  2272  sbel2x  2503  eu6  2599  moanmo  2647  2eu3  2678  2eu7  2682  2eu8  2683  eq2tri  2822  r19.42v  3194  rexcomf  3301  rabswap  3421  spc2ed  3555  euxfr2w  3677  euxfr2  3679  rmo4  3687  reu8  3690  rmo3f  3691  reuxfrd  3705  rmo3  3835  difin2  4246  rcompleq  4250  euelss  4277  ssunsn  4783  uniprg  4882  inuni  5310  eqvinop  5455  eqvinot  5456  elxp2  5674  opeliun2xp  5718  elvvv  5726  brinxp2  5728  dmuni  5895  imadmrnOLD  6067  asymref2  6110  cnvopab  6130  cnvxp  6146  cnvxpOLD  6147  xpdifid  6158  xpdifcnvepel  6159  cnvcnvsn  6220  opswap  6230  mptpreima  6239  xpco  6292  dfpo2  6299  fncnv  6614  fnres  6667  mptfnf  6675  dff1o2  6831  f13dfv  7283  fliftcnv  7320  isoini  7347  elrnmpores  7559  ndmovcom  7609  uniuni  7777  opabex3rd  7979  mptmpoopabbrd  8095  fsplit  8131  brtpos  8256  tposmpo  8284  oaord  8559  nnaord  8632  naddasslem1  8708  naddasslem2  8709  brinxper  8751  pmex  8856  mapsnend  9068  snmapen  9070  xpsnen  9084  xpcomco  9090  elfi2  9410  supmo  9448  infmo  9493  frind  9758  cp  9958  dfac5lem1  10206  dfac5lem2  10207  dfac2b  10213  kmlem3  10235  cflim3  10344  brdom7disj  10614  brdom6disj  10615  recmulnq  11053  lesub0  11837  wloglei  11852  creur  12318  indstr  13047  xmulcom  13400  xmulneg1  13403  xmulf  13406  iccneg  13607  fzrev  13725  injresinj  13930  sgn3da  15260  rediv  15304  imdiv  15311  lenegsq  15494  o1lo1  15710  fsumcom2  15946  fsumcom  15947  fprodcom2  16157  fprodcom  16158  divalglem10  16578  smueqlem  16666  gcdcom  16691  lcmcom  16774  isprm2  16863  isprm7  16890  infpn2  17097  imasleval  17719  dfiso3  17954  posglbmo  18590  odulatb  18614  oduclatb  18687  oppgid  19576  gsumcom  20197  gsumcom3  20198  dfring3  20524  dfrhm2  20710  isdrng5  21014  isfieldidl  21546  xrsdsreclb  21726  opsrtoslem1  22370  psdmvr  22496  madutpos  22963  fvmptnn04if  23173  ntreq0  23401  ist0-3  23669  txkgen  23977  trfil2  24212  flimrest  24308  blres  24756  metrest  24849  restmetu  24895  elii1  25262  isclmp  25424  evthicc2  25787  ovolfcl  25793  dyaddisj  25923  iblpos  26119  itgposval  26122  ditgsplit  26187  itgsubst  26375  sincosq3sgn  26835  cos11  26867  dvdsflsumcom  27521  fsumvma  27546  logfaclbnd  27555  dchrelbas3  27571  lgsdi  27667  lgsquadlem3  27715  2lgslem1a  27724  lestri3  28118  ltsrec  28193  istrkg2ld  28928  tgjustf  28941  tgcgr4  29000  mirreu3  29132  hpgcom  29251  colhp  29254  dfcgra2  29344  prlngsym  29425  dfprlng2  29431  nbgrel  29927  nbgrsym  29950  wlkson  30241  dfpth2  30320  isspthonpth  30341  usgr2pth0  30357  wwlksnextinj  30494  elwspths2spth  30565  rusgrnumwwlkl1  30566  clwwlknclwwlkdifnum  30577  clwwlkn1  30638  clwwlkn2  30641  iseupthf1o  30809  eupth2lem2  30826  frgrncvvdeqlem2  30907  fusgr2wsp2nb  30941  fusgreg2wsp  30943  frgrreg  31001  frgrregord013  31002  h2hcau  31587  nmopub  32516  nmfnleub  32533  chrelati  32972  cvexchlem  32976  mdsymlem8  33018  sumdmdii  33023  2reucom  33124  reuxfrdf  33135  dmrab  33141  difrab2  33142  ififcom  33194  ressupprn  33331  2ndpreima  33349  fpwrelmapffslem  33371  xrofsup  33406  mgccnv  33607  pmtrprfv2  33696  smatrcl  34475  cnvordtrestixx  34592  issgon  34802  eulerpartlemr  35053  eulerpartlemgvv  35055  ballotlem2  35168  oddprm2  35331  bnj257  35385  bnj545  35572  bnj594  35589  nfan1c  35750  fwfffunres  35765  satfv0  36210  satfvsuclem1  36211  dfdm5  36630  dfrn5  36631  elima4  36633  elfix  36758  dffix2  36760  brimg  36792  lemsuccf  36796  dfrecs2  36807  dfrdg4  36808  cgrcomlr  36856  ofscom  36865  btwnexch  36883  fscgr  36938  bj-df-ifc  37543  bj-axseprep  38083  bj-dfmpoa  38133  bj-eldiag  38191  bj-imdirco  38205  bj-ccinftydisj  38228  mptsnunlem  38355  topdifinffinlem  38364  fvineqsneq  38429  wl-cases2-dnf  38538  fin2solem  38623  poimirlem26  38658  poimirlem30  38662  poimirlem32  38664  ftc1anclem6  38710  ftc1anc  38713  heibor1  38838  isdrngo3  38987  isdmn3  39102  anan  39261  br1cnvinxp  39285  raldmqseu  39391  inxpxrn  39444  prtlem70  40008  lrelat  40165  islshpat  40168  atlrelat1  40472  ishlat2  40504  cdlemb3  41757  diblsmopel  42322  dicelval3  42331  diclspsn  42345  uzindd  43122  3factsumint2  43166  3factsumint3  43167  3factsumint  43169  fimgmcyc  43692  eu6w  43781  fz1eqin  43874  diophrex  43880  fphpd  43917  fzneg  44083  expdioph  44124  dford4  44130  lnr2i  44212  fgraphopab  44299  omge2  44394  oadif1lem  44475  oadif1  44476  ifpancor  44559  ifpidg  44586  ifpid2g  44588  ifpid1g  44589  ifpim23g  44590  rp-fakeoranass  44609  minregex  44629  dfid7  44706  dfrtrcl5  44723  relexp0eq  44795  fsovrfovd  45103  rr-grothprimbi  45373  uunT1p1  45857  uun132p1  45862  un2122  45866  uun2131p1  45868  uunT12p1  45876  uunT12p2  45877  uunT12p3  45878  uun2221  45889  uun2221p1  45890  uun2221p2  45891  3impdirp1  45892  ancomstVD  45941  icccncfext  46991  dvnmul  47047  dvmptfprodlem  47048  dvnprodlem2  47051  fourierdlem42  47253  fourierdlem83  47293  f1cof1b  48241  2reu3  48274  2reu7  48275  2reu8  48276  2reuimp0  48278  ndmaovcom  48369  an4com24  48432  4an21  48434  sprvalpwn0  48659  prpair  48677  prproropf1olem0  48678  clnbgrel  49020  clnbgrsym  49030  2zrngnmrid  49447  isidom3  49536  rrx2linest  49948  pm5.32rda  49998  resinsnALT  50080  catcinv  50628  thincsect2  50697  lmdfval  50926  cmdfval  50927  2alsraln0  51082