MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ancom Structured version   Visualization version   GIF version

Theorem ancom 464
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
StepHypRef Expression
1 pm3.22 463 . 2 ((𝜑𝜓) → (𝜓𝜑))
2 pm3.22 463 . 2 ((𝜓𝜑) → (𝜑𝜓))
31, 2impbii 212 1 ((𝜑𝜓) ↔ (𝜓𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 209  wa 399
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 400
This theorem is referenced by:  ancomd  465  biancomi  466  biancomd  467  ancomst  468  pm4.71r  562  pm5.32ri  579  pm5.32rd  581  bianassc  642  an12  644  an13  646  an42  656  andir  1006  cases2  1043  dfifp6  1064  ifpn  1069  excxor  1508  cador  1610  cadcoma  1614  exancom  1862  19.42v  1955  19.42  2240  sbel2x  2500  eu6  2660  moanmo  2710  2eu3  2741  2eu7  2746  2eu8  2747  eq2tri  2886  r19.28vOLD  3182  r19.29rOLD  3250  r19.42v  3341  rexcomOLD  3347  rexcomf  3349  rabswap  3474  spc2ed  3588  euxfr2w  3697  euxfr2  3699  rmo4  3707  reu8  3710  rmo3f  3711  reuxfrd  3725  rmo3  3856  incomOLD  4164  difin2  4251  euelss  4275  ssunsn  4745  inuni  5232  eqvinop  5365  elxp2  5566  elvvv  5614  brinxp2  5616  dmuni  5770  imadmrn  5926  asymref2  5964  cnvxp  6001  xpdifid  6012  cnvcnvsn  6063  opswap  6073  mptpreima  6079  xpco  6127  fncnv  6415  fnres  6463  mptfnf  6472  dff1o2  6611  f13dfv  7023  fliftcnv  7057  isoini  7084  elrnmpores  7281  ndmovcom  7329  uniuni  7478  opabex3rd  7662  mptmpoopabbrd  7774  fsplit  7808  brtpos  7897  tposmpo  7925  oaord  8169  nnaord  8241  pmex  8407  mapsnend  8584  snmapen  8586  xpsnen  8597  xpcomco  8603  elfi2  8875  supmo  8913  infmo  8956  cp  9317  dfac5lem1  9547  dfac5lem2  9548  dfac2b  9554  kmlem3  9576  cflim3  9682  brdom7disj  9951  brdom6disj  9952  recmulnq  10384  lesub0  11155  wloglei  11170  creur  11628  indstr  12313  xmulcom  12656  xmulneg1  12659  xmulf  12662  iccneg  12859  fzrev  12974  injresinj  13162  rediv  14490  imdiv  14497  lenegsq  14680  o1lo1  14894  fsumcom2  15129  fsumcom  15130  fprodcom2  15338  fprodcom  15339  divalglem10  15751  smueqlem  15837  gcdcom  15860  lcmcom  15935  isprm2  16024  isprm7  16050  infpn2  16247  imasleval  16814  dfiso3  17043  odulatb  17753  oduclatb  17754  posglbmo  17757  oppgid  18484  gsumcom  19097  gsumcom3  19098  dfrhm2  19472  opsrtoslem1  20264  xrsdsreclb  20592  madutpos  21251  fvmptnn04if  21457  ntreq0  21685  ist0-3  21953  txkgen  22260  trfil2  22495  flimrest  22591  blres  23041  metrest  23134  restmetu  23180  elii1  23543  isclmp  23705  evthicc2  24067  ovolfcl  24073  dyaddisj  24203  iblpos  24399  itgposval  24402  ditgsplit  24467  itgsubst  24655  sincosq3sgn  25096  cos11  25128  dvdsflsumcom  25776  fsumvma  25800  logfaclbnd  25809  dchrelbas3  25825  lgsdi  25921  lgsquadlem3  25969  2lgslem1a  25978  istrkg2ld  26257  tgjustf  26270  tgcgr4  26328  mirreu3  26451  hpgcom  26564  colhp  26567  dfcgra2  26627  nbgrel  27133  nbgrsym  27156  wlkson  27449  isspthonpth  27541  usgr2pth0  27557  wwlksnextinj  27688  elwspths2spth  27756  rusgrnumwwlkl1  27757  clwwlknclwwlkdifnum  27768  clwwlkn1  27829  clwwlkn2  27832  iseupthf1o  27990  eupth2lem2  28007  frgrncvvdeqlem2  28088  fusgr2wsp2nb  28122  fusgreg2wsp  28124  frgrreg  28182  frgrregord013  28183  h2hcau  28765  nmopub  29694  nmfnleub  29711  chrelati  30150  cvexchlem  30154  mdsymlem8  30196  sumdmdii  30201  nelbOLD  30241  2reucom  30252  reuxfrdf  30264  dmrab  30269  difrab2  30270  2ndpreima  30454  fpwrelmapffslem  30479  xrofsup  30503  mcgcnv  30690  pmtrprfv2  30764  smatrcl  31121  cnvordtrestixx  31213  issgon  31439  eulerpartlemr  31689  eulerpartlemgvv  31691  ballotlem2  31803  sgn3da  31856  oddprm2  31983  bnj257  32034  bnj545  32224  bnj594  32241  satfv0  32662  satfvsuclem1  32663  dfpo2  33048  dfdm5  33073  dfrn5  33074  elima4  33076  frind  33142  sletri3  33291  nocvxmin  33305  sltrec  33335  elfix  33421  dffix2  33423  brimg  33455  brsuccf  33459  dfrecs2  33468  dfrdg4  33469  cgrcomlr  33516  ofscom  33525  btwnexch  33543  fscgr  33598  bj-df-ifc  33970  bj-dfmpoa  34478  bj-eldiag  34536  bj-imdirco  34550  bj-ccinftydisj  34573  mptsnunlem  34700  topdifinffinlem  34709  fvineqsneq  34774  wl-cases2-dnf  34862  wl-ax11-lem4  34930  fin2solem  34988  poimirlem4  35006  poimirlem26  35028  poimirlem30  35032  poimirlem32  35034  ftc1anclem6  35080  ftc1anc  35083  heibor1  35193  isdrngo3  35342  isdmn3  35457  an2anr  35603  anan  35604  inxpxrn  35748  prtlem70  36098  lrelat  36255  islshpat  36258  atlrelat1  36562  ishlat2  36594  cdlemb3  37847  diblsmopel  38412  dicelval3  38421  diclspsn  38435  uzindd  39209  3factsumint2  39258  3factsumint3  39259  3factsumint  39261  fz1eqin  39626  diophrex  39632  fphpd  39673  fzneg  39839  expdioph  39880  dford4  39886  lnr2i  39976  fgraphopab  40070  ifpancor  40088  ifpidg  40115  ifpid2g  40117  ifpid1g  40118  ifpim23g  40119  rp-fakeoranass  40138  dfid7  40228  dfrtrcl5  40245  relexp0eq  40318  fsovrfovd  40627  rcompleq  40642  rr-grothprimbi  40923  uunT1p1  41407  uun132p1  41412  un2122  41416  uun2131p1  41418  uunT12p1  41426  uunT12p2  41427  uunT12p3  41428  uun2221  41439  uun2221p1  41440  uun2221p2  41441  3impdirp1  41442  ancomstVD  41491  icccncfext  42455  dvnmul  42511  dvmptfprodlem  42512  dvnprodlem2  42515  fourierdlem42  42717  fourierdlem83  42757  2reu3  43592  2reu7  43593  2reu8  43594  2reuimp0  43596  ndmaovcom  43687  an4com24  43750  4an21  43752  sprvalpwn0  43926  prpair  43944  prproropf1olem0  43945  2zrngnmrid  44500  opeliun2xp  44660  rrx2linest  45082
  Copyright terms: Public domain W3C validator