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  1026  cases2  1063  dfifp6  1084  ifpn  1090  13an22anass  1379  4anpull2OLD  1383  excxor  1546  cador  1638  cadcoma  1642  exancom  1891  19.42v  1983  19.42  2272  sbel2x  2506  eu6  2602  moanmo  2650  2eu3  2681  2eu7  2685  2eu8  2686  eq2tri  2825  r19.42v  3197  rexcomf  3304  rabswap  3425  spc2ed  3560  euxfr2w  3683  euxfr2  3685  rmo4  3693  reu8  3696  rmo3f  3697  reuxfrd  3711  rmo3  3842  difin2  4254  rcompleq  4258  euelss  4285  ssunsn  4794  uniprg  4888  inuni  5320  eqvinop  5469  elxp2  5685  opeliun2xp  5729  elvvv  5737  brinxp2  5739  dmuni  5904  imadmrn  6072  asymref2  6117  cnvopab  6137  cnvxp  6154  xpdifid  6165  xpdifcnvepel  6166  cnvcnvsn  6220  opswap  6230  mptpreima  6239  xpco  6290  dfpo2  6297  fncnv  6609  fnres  6662  mptfnf  6670  dff1o2  6826  f13dfv  7272  fliftcnv  7309  isoini  7336  elrnmpores  7548  ndmovcom  7597  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  10241  brdom7disj  10510  brdom6disj  10511  recmulnq  10944  lesub0  11726  wloglei  11741  creur  12207  indstr  12935  xmulcom  13287  xmulneg1  13290  xmulf  13293  iccneg  13494  fzrev  13611  injresinj  13816  sgn3da  15134  rediv  15178  imdiv  15185  lenegsq  15368  o1lo1  15584  fsumcom2  15821  fsumcom  15822  fprodcom2  16034  fprodcom  16035  divalglem10  16455  smueqlem  16543  gcdcom  16566  lcmcom  16646  isprm2  16735  isprm7  16762  infpn2  16968  imasleval  17590  dfiso3  17825  posglbmo  18461  odulatb  18485  oduclatb  18558  oppgid  19421  gsumcom  20042  gsumcom3  20043  dfrhm2  20552  isdrng5  20854  isfieldidl  21386  xrsdsreclb  21564  opsrtoslem1  22206  psdmvr  22332  madutpos  22799  fvmptnn04if  23006  ntreq0  23234  ist0-3  23502  txkgen  23809  trfil2  24044  flimrest  24140  blres  24588  metrest  24681  restmetu  24727  elii1  25094  isclmp  25256  evthicc2  25619  ovolfcl  25625  dyaddisj  25755  iblpos  25952  itgposval  25955  ditgsplit  26020  itgsubst  26208  sincosq3sgn  26665  cos11  26698  dvdsflsumcom  27352  fsumvma  27377  logfaclbnd  27386  dchrelbas3  27402  lgsdi  27498  lgsquadlem3  27546  2lgslem1a  27555  lestri3  27919  ltsrec  27994  istrkg2ld  28729  tgjustf  28742  tgcgr4  28800  mirreu3  28931  hpgcom  29049  colhp  29052  dfcgra2  29141  prlngsym  29191  dfprlng2  29197  nbgrel  29690  nbgrsym  29713  wlkson  30004  dfpth2  30078  isspthonpth  30098  usgr2pth0  30114  wwlksnextinj  30248  elwspths2spth  30319  rusgrnumwwlkl1  30320  clwwlknclwwlkdifnum  30331  clwwlkn1  30392  clwwlkn2  30395  iseupthf1o  30553  eupth2lem2  30570  frgrncvvdeqlem2  30651  fusgr2wsp2nb  30685  fusgreg2wsp  30687  frgrreg  30745  frgrregord013  30746  h2hcau  31331  nmopub  32260  nmfnleub  32277  chrelati  32716  cvexchlem  32720  mdsymlem8  32762  sumdmdii  32767  2reucom  32826  reuxfrdf  32837  dmrab  32843  difrab2  32844  ififcom  32896  ressupprn  33035  2ndpreima  33053  fpwrelmapffslem  33077  xrofsup  33112  mgccnv  33319  pmtrprfv2  33408  smatrcl  34186  cnvordtrestixx  34303  issgon  34513  eulerpartlemr  34764  eulerpartlemgvv  34766  ballotlem2  34879  oddprm2  35042  bnj257  35096  bnj545  35283  bnj594  35300  nfan1c  35461  satfv0  35850  satfvsuclem1  35851  dfdm5  36265  dfrn5  36266  elima4  36268  elfix  36393  dffix2  36395  brimg  36427  lemsuccf  36431  dfrecs2  36442  dfrdg4  36443  cgrcomlr  36490  ofscom  36499  btwnexch  36517  fscgr  36572  bj-df-ifc  37173  bj-axseprep  37711  bj-dfmpoa  37760  bj-eldiag  37820  bj-imdirco  37834  bj-ccinftydisj  37857  mptsnunlem  37984  topdifinffinlem  37993  fvineqsneq  38058  wl-cases2-dnf  38167  fin2solem  38257  poimirlem26  38297  poimirlem30  38301  poimirlem32  38303  ftc1anclem6  38349  ftc1anc  38352  heibor1  38461  isdrngo3  38610  isdmn3  38725  anan  38884  br1cnvinxp  38908  raldmqseu  39014  inxpxrn  39067  prtlem70  39631  lrelat  39788  islshpat  39791  atlrelat1  40095  ishlat2  40127  cdlemb3  41380  diblsmopel  41945  dicelval3  41954  diclspsn  41968  uzindd  42745  3factsumint2  42789  3factsumint3  42790  3factsumint  42792  fimgmcyc  43302  eu6w  43408  fz1eqin  43500  diophrex  43506  fphpd  43543  fzneg  43709  expdioph  43750  dford4  43756  lnr2i  43843  fgraphopab  43930  omge2  44025  oadif1lem  44106  oadif1  44107  ifpancor  44190  ifpidg  44217  ifpid2g  44219  ifpid1g  44220  ifpim23g  44221  rp-fakeoranass  44240  minregex  44260  dfid7  44338  dfrtrcl5  44355  relexp0eq  44427  fsovrfovd  44735  rr-grothprimbi  45005  uunT1p1  45489  uun132p1  45494  un2122  45498  uun2131p1  45500  uunT12p1  45508  uunT12p2  45509  uunT12p3  45510  uun2221  45521  uun2221p1  45522  uun2221p2  45523  3impdirp1  45524  ancomstVD  45573  icccncfext  46601  dvnmul  46657  dvmptfprodlem  46658  dvnprodlem2  46661  fourierdlem42  46863  fourierdlem83  46903  f1cof1b  47814  2reu3  47847  2reu7  47848  2reu8  47849  2reuimp0  47851  ndmaovcom  47942  an4com24  48005  4an21  48007  sprvalpwn0  48232  prpair  48250  prproropf1olem0  48251  clnbgrel  48593  clnbgrsym  48603  2zrngnmrid  49021  isidom3  49110  rrx2linest  49522  pm5.32dav  49572  resinsnALT  49651  catcinv  50177  thincsect2  50246  lmdfval  50427  cmdfval  50428  2alsraln0  50595