Theorem ancom 465

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

Syntax hints:   ↔ wb 209   ∧ wa 400

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 401

This theorem is referenced by:  ancomd  466  biancomi  467  biancomd  468  ancomst  469  pm4.71r  567  pm5.32ri  585  pm5.32rd  588  an2anr  647  bianassc  655  an12  657  an13  659  an42  669  andir  1024  cases2  1061  dfifp6  1082  ifpn  1088  13an22anass  1377  4anpull2OLD  1381  excxor  1543  cador  1635  cadcoma  1639  exancom  1888  19.42v  1980  19.42  2278  sbel2x  2512  eu6  2608  moanmo  2656  2eu3  2687  2eu7  2691  2eu8  2692  eq2tri  2831  r19.42v  3203  rexcomf  3310  rabswap  3432  spc2ed  3569  euxfr2w  3692  euxfr2  3694  rmo4  3702  reu8  3705  rmo3f  3706  reuxfrd  3720  rmo3  3851  difin2  4262  rcompleq  4266  euelss  4293  ssunsn  4795  uniprg  4889  inuni  5318  eqvinop  5467  elxp2  5683  opeliun2xp  5727  elvvv  5735  brinxp2  5737  dmuni  5902  imadmrn  6070  asymref2  6115  cnvopab  6135  cnvxp  6152  xpdifid  6163  xpdifcnvepel  6164  cnvcnvsn  6218  opswap  6228  mptpreima  6237  xpco  6288  dfpo2  6295  fncnv  6607  fnres  6660  mptfnf  6668  dff1o2  6824  f13dfv  7270  fliftcnv  7307  isoini  7334  elrnmpores  7546  ndmovcom  7595  uniuni  7757  opabex3rd  7959  mptmpoopabbrd  8074  fsplit  8108  brtpos  8227  tposmpo  8255  oaord  8528  nnaord  8601  naddasslem1  8677  naddasslem2  8678  brinxper  8720  pmex  8825  mapsnend  9029  snmapen  9031  xpsnen  9045  xpcomco  9051  elfi2  9370  supmo  9408  infmo  9453  frind  9718  cp  9873  dfac5lem1  10103  dfac5lem2  10104  dfac2b  10110  kmlem3  10132  cflim3  10242  brdom7disj  10511  brdom6disj  10512  recmulnq  10945  lesub0  11727  wloglei  11742  creur  12208  indstr  12936  xmulcom  13288  xmulneg1  13291  xmulf  13294  iccneg  13495  fzrev  13611  injresinj  13816  sgn3da  15134  rediv  15178  imdiv  15185  lenegsq  15368  o1lo1  15584  fsumcom2  15821  fsumcom  15822  fprodcom2  16034  fprodcom  16035  divalglem10  16456  smueqlem  16544  gcdcom  16567  lcmcom  16647  isprm2  16736  isprm7  16763  infpn2  16969  imasleval  17591  dfiso3  17826  posglbmo  18462  odulatb  18486  oduclatb  18559  oppgid  19422  gsumcom  20043  gsumcom3  20044  dfrhm2  20552  xrsdsreclb  21529  opsrtoslem1  22171  psdmvr  22297  madutpos  22764  fvmptnn04if  22971  ntreq0  23199  ist0-3  23467  txkgen  23774  trfil2  24009  flimrest  24105  blres  24553  metrest  24646  restmetu  24692  elii1  25059  isclmp  25221  evthicc2  25584  ovolfcl  25590  dyaddisj  25720  iblpos  25917  itgposval  25920  ditgsplit  25985  itgsubst  26173  sincosq3sgn  26627  cos11  26660  dvdsflsumcom  27314  fsumvma  27339  logfaclbnd  27348  dchrelbas3  27364  lgsdi  27460  lgsquadlem3  27508  2lgslem1a  27517  lestri3  27881  ltsrec  27956  istrkg2ld  28691  tgjustf  28704  tgcgr4  28762  mirreu3  28889  hpgcom  29004  colhp  29007  dfcgra2  29094  prlngsym  29142  nbgrel  29627  nbgrsym  29650  wlkson  29941  dfpth2  30015  isspthonpth  30035  usgr2pth0  30051  wwlksnextinj  30185  elwspths2spth  30256  rusgrnumwwlkl1  30257  clwwlknclwwlkdifnum  30268  clwwlkn1  30329  clwwlkn2  30332  iseupthf1o  30490  eupth2lem2  30507  frgrncvvdeqlem2  30588  fusgr2wsp2nb  30622  fusgreg2wsp  30624  frgrreg  30682  frgrregord013  30683  h2hcau  31268  nmopub  32197  nmfnleub  32214  chrelati  32653  cvexchlem  32657  mdsymlem8  32699  sumdmdii  32704  2reucom  32763  reuxfrdf  32774  dmrab  32780  difrab2  32781  ififcom  32833  ressupprn  32972  2ndpreima  32990  fpwrelmapffslem  33014  xrofsup  33049  mgccnv  33256  pmtrprfv2  33345  smatrcl  34127  cnvordtrestixx  34244  issgon  34454  eulerpartlemr  34705  eulerpartlemgvv  34707  ballotlem2  34820  oddprm2  34983  bnj257  35037  bnj545  35224  bnj594  35241  nfan1c  35402  satfv0  35745  satfvsuclem1  35746  dfdm5  36160  dfrn5  36161  elima4  36163  elfix  36288  dffix2  36290  brimg  36322  lemsuccf  36326  dfrecs2  36337  dfrdg4  36338  cgrcomlr  36385  ofscom  36394  btwnexch  36412  fscgr  36467  bj-df-ifc  37058  bj-axseprep  37594  bj-dfmpoa  37643  bj-eldiag  37703  bj-imdirco  37717  bj-ccinftydisj  37740  mptsnunlem  37867  topdifinffinlem  37876  fvineqsneq  37941  wl-cases2-dnf  38050  fin2solem  38140  poimirlem26  38180  poimirlem30  38184  poimirlem32  38186  ftc1anclem6  38232  ftc1anc  38235  heibor1  38344  isdrngo3  38493  isdmn3  38608  anan  38769  br1cnvinxp  38793  raldmqseu  38899  inxpxrn  38952  prtlem70  39516  lrelat  39673  islshpat  39676  atlrelat1  39980  ishlat2  40012  cdlemb3  41265  diblsmopel  41830  dicelval3  41839  diclspsn  41853  uzindd  42630  3factsumint2  42674  3factsumint3  42675  3factsumint  42677  fimgmcyc  43189  eu6w  43295  fz1eqin  43387  diophrex  43393  fphpd  43430  fzneg  43596  expdioph  43637  dford4  43643  lnr2i  43730  fgraphopab  43817  omge2  43912  oadif1lem  43993  oadif1  43994  ifpancor  44077  ifpidg  44104  ifpid2g  44106  ifpid1g  44107  ifpim23g  44108  rp-fakeoranass  44127  minregex  44147  dfid7  44225  dfrtrcl5  44242  relexp0eq  44314  fsovrfovd  44622  rr-grothprimbi  44892  uunT1p1  45376  uun132p1  45381  un2122  45385  uun2131p1  45387  uunT12p1  45395  uunT12p2  45396  uunT12p3  45397  uun2221  45408  uun2221p1  45409  uun2221p2  45410  3impdirp1  45411  ancomstVD  45460  icccncfext  46488  dvnmul  46544  dvmptfprodlem  46545  dvnprodlem2  46548  fourierdlem42  46750  fourierdlem83  46790  f1cof1b  47698  2reu3  47731  2reu7  47732  2reu8  47733  2reuimp0  47735  ndmaovcom  47826  an4com24  47889  4an21  47891  sprvalpwn0  48116  prpair  48134  prproropf1olem0  48135  clnbgrel  48477  clnbgrsym  48487  2zrngnmrid  48905  rrx2linest  49402  pm5.32dav  49452  resinsnALT  49531  catcinv  50057  thincsect2  50126  lmdfval  50307  cmdfval  50308