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  13an22anassOLD  1380  4anpull2OLD  1384  excxor  1546  cador  1641  cadcoma  1645  exancom  1894  19.42v  1988  19.42  2276  sbel2x  2506  eu6  2602  moanmo  2650  2eu3  2681  2eu7  2685  2eu8  2686  eq2tri  2825  r19.42v  3198  rexcomf  3305  rabswap  3425  spc2ed  3559  euxfr2w  3681  euxfr2  3683  rmo4  3691  reu8  3694  rmo3f  3695  reuxfrd  3709  rmo3  3840  difin2  4249  rcompleq  4253  euelss  4280  ssunsn  4789  uniprg  4888  inuni  5318  eqvinop  5463  eqvinot  5464  elxp2  5682  opeliun2xp  5726  elvvv  5735  brinxp2  5737  dmuni  5908  imadmrnOLD  6086  asymref2  6129  cnvopab  6149  cnvxp  6165  cnvxpOLD  6166  xpdifid  6177  xpdifcnvepel  6178  cnvcnvsn  6239  opswap  6249  mptpreima  6258  xpco  6318  dfpo2  6325  fncnv  6643  fnres  6696  mptfnf  6704  dff1o2  6860  f13dfv  7313  fliftcnv  7350  isoini  7377  elrnmpores  7590  ndmovcom  7640  uniuni  7808  opabex3rd  8012  mptmpoopabbrd  8129  fsplit  8165  brtpos  8290  tposmpo  8318  oaord  8593  nnaord  8666  naddasslem1  8742  naddasslem2  8743  brinxper  8785  pmex  8890  mapsnend  9102  snmapen  9104  xpsnen  9118  xpcomco  9124  elfi2  9443  supmo  9481  infmo  9526  frind  9791  cp  9991  dfac5lem1  10241  dfac5lem2  10242  dfac2b  10248  kmlem3  10270  cflim3  10379  brdom7disj  10649  brdom6disj  10650  recmulnq  11088  lesub0  11873  wloglei  11888  creur  12354  indstr  13083  xmulcom  13436  xmulneg1  13439  xmulf  13442  iccneg  13643  fzrev  13761  injresinj  13966  sgn3da  15297  rediv  15341  imdiv  15348  lenegsq  15531  o1lo1  15748  fsumcom2  15984  fsumcom  15985  fprodcom2  16195  fprodcom  16196  divalglem10  16616  smueqlem  16704  gcdcom  16729  lcmcom  16812  isprm2  16901  isprm7  16928  infpn2  17135  imasleval  17763  dfiso3  17998  posglbmo  18634  odulatb  18658  oduclatb  18731  oppgid  19621  gsumcom  20242  gsumcom3  20243  dfring3  20569  dfrhm2  20755  isdrng5  21059  isfieldidl  21591  xrsdsreclb  21772  opsrtoslem1  22419  psdmvr  22545  madutpos  23012  fvmptnn04if  23222  ntreq0  23450  ist0-3  23718  txkgen  24026  trfil2  24261  flimrest  24357  blres  24805  metrest  24898  restmetu  24944  elii1  25311  isclmp  25473  evthicc2  25836  ovolfcl  25842  dyaddisj  25972  iblpos  26168  itgposval  26171  ditgsplit  26236  itgsubst  26424  sincosq3sgn  26886  cos11  26918  dvdsflsumcom  27572  fsumvma  27597  logfaclbnd  27606  dchrelbas3  27622  lgsdi  27718  lgsquadlem3  27766  2lgslem1a  27775  lestri3  28169  ltsrec  28244  istrkg2ld  28979  tgjustf  28992  tgcgr4  29051  mirreu3  29183  hpgcom  29302  colhp  29305  dfcgra2  29395  prlngsym  29476  dfprlng2  29482  nbgrel  29978  nbgrsym  30001  wlkson  30292  dfpth2  30371  isspthonpth  30392  usgr2pth0  30408  wwlksnextinj  30545  elwspths2spth  30616  rusgrnumwwlkl1  30617  clwwlknclwwlkdifnum  30628  clwwlkn1  30689  clwwlkn2  30692  iseupthf1o  30860  eupth2lem2  30877  frgrncvvdeqlem2  30958  fusgr2wsp2nb  30992  fusgreg2wsp  30994  frgrreg  31052  frgrregord013  31053  h2hcau  31638  nmopub  32567  nmfnleub  32584  chrelati  33023  cvexchlem  33027  mdsymlem8  33069  sumdmdii  33074  2reucom  33175  reuxfrdf  33186  dmrab  33192  difrab2  33193  ififcom  33244  ressupprn  33380  2ndpreima  33398  fpwrelmapffslem  33420  xrofsup  33455  mgccnv  33659  pmtrprfv2  33748  smatrcl  34539  cnvordtrestixx  34656  issgon  34866  eulerpartlemr  35117  eulerpartlemgvv  35119  ballotlem2  35232  oddprm2  35395  bnj257  35449  bnj545  35636  bnj594  35653  nfan1c  35814  fwfffunres  35829  satfv0  36331  satfvsuclem1  36332  mirimanofffr  36670  dfdm5  36752  dfrn5  36753  elima4  36755  elfix  36880  dffix2  36882  brimg  36914  lemsuccf  36918  dfrecs2  36929  dfrdg4  36930  cgrcomlr  36978  ofscom  36987  btwnexch  37005  fscgr  37060  bj-df-ifc  37665  coi2res  38200  bj-axseprep  38260  bj-dfmpoa  38310  bj-eldiag  38365  bj-imdirco  38379  bj-ccinftydisj  38402  mptsnunlem  38529  topdifinffinlem  38538  fvineqsneq  38603  wl-cases2-dnf  38712  fin2solem  38797  poimirlem26  38832  poimirlem30  38836  poimirlem32  38838  ftc1anclem6  38884  ftc1anc  38887  heibor1  39010  isdrngo3  39159  isdmn3  39274  anan  39433  br1cnvinxp  39457  raldmqseu  39563  inxpxrn  39616  prtlem70  40180  lrelat  40337  islshpat  40340  atlrelat1  40644  ishlat2  40676  cdlemb3  41929  diblsmopel  42494  dicelval3  42503  diclspsn  42517  uzindd  43294  3factsumint2  43338  3factsumint3  43339  3factsumint  43341  fimgmcyc  43864  eu6w  43953  fz1eqin  44046  diophrex  44052  fphpd  44089  fzneg  44255  expdioph  44296  dford4  44302  lnr2i  44383  fgraphopab  44466  omge2  44561  oadif1lem  44642  oadif1  44643  ifpancor  44726  ifpidg  44753  ifpid2g  44755  ifpid1g  44756  ifpim23g  44757  rp-fakeoranass  44776  minregex  44796  dfid7  44873  dfrtrcl5  44890  relexp0eq  44962  fsovrfovd  45270  rr-grothprimbi  45540  uunT1p1  46023  uun132p1  46028  un2122  46032  uun2131p1  46034  uunT12p1  46042  uunT12p2  46043  uunT12p3  46044  uun2221  46055  uun2221p1  46056  uun2221p2  46057  3impdirp1  46058  ancomstVD  46107  icccncfext  47170  dvnmul  47226  dvmptfprodlem  47227  dvnprodlem2  47230  fourierdlem42  47432  fourierdlem83  47472  f1cof1b  48420  2reu3  48454  2reu7  48455  2reu8  48456  2reuimp0  48458  ndmaovcom  48548  an4com24  48611  4an21  48613  sprvalpwn0  48838  prpair  48856  prproropf1olem0  48857  clnbgrel  49199  clnbgrsym  49209  2zrngnmrid  49626  isidom3  49773  rrx2linest  50185  pm5.32rda  50235  resinsnALT  50317  catcinv  50865  thincsect2  50934  lmdfval  51163  cmdfval  51164  2alsraln0  51341