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

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
StepHypRef Expression
1 pm3.22 465 . 2 ((𝜑𝜓) → (𝜓𝜑))
2 pm3.22 465 . 2 ((𝜓𝜑) → (𝜑𝜓))
31, 2impbii 199 1 ((𝜑𝜓) ↔ (𝜓𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 384
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 197  df-an 386
This theorem is referenced by:  ancomd  467  ancomst  468  ancomsd  470  pm4.71r  662  pm5.32ri  669  pm5.32rd  671  anbi2ci  731  anbi12ci  733  an12  837  an32  838  an13  839  an42  865  andir  911  dfbi3OLD  994  dfifp6  1017  3anrot  1041  3ancoma  1043  nancom  1447  excxor  1466  cador  1544  cadcoma  1548  exancom  1784  19.42v  1915  19.42  2103  sbel2x  2458  moanmo  2531  2eu3  2554  2eu7  2558  2eu8  2559  eq2tri  2682  r19.28v  3064  r19.29r  3066  r19.42v  3084  rexcomf  3089  rabswap  3110  euxfr2  3373  rmo4  3381  reu8  3384  rmo3  3509  incom  3783  difin2  3866  euelss  3890  ssunsn  4328  inuni  4786  reuxfr2d  4851  eqvinop  4915  dfid3  4990  elxp2  5092  elvvv  5139  brinxp2  5141  dmuni  5294  dfres2  5412  restidsing  5417  dfima2  5427  imadmrn  5435  imai  5437  asymref2  5472  cnvxp  5510  xpdifid  5521  cnvcnvsn  5571  opswap  5581  mptpreima  5587  rnco  5600  ressn  5630  xpco  5634  wfi  5672  elon2  5693  fncnv  5920  fununi  5922  fnres  5965  mptfnf  5972  fnopabg  5974  dff1o2  6099  eqfnfv3  6269  respreima  6300  fsn  6356  f13dfv  6484  fliftcnv  6515  isoini  6542  elrnmpt2res  6727  ndmovcom  6774  uniuni  6920  mptmpt2opabbrd  7193  brtpos2  7303  brtpos  7306  tpostpos  7317  tposmpt2  7334  mpt2curryd  7340  oaord  7572  oeeu  7628  nnaord  7644  pmex  7807  elpmg  7817  mapval2  7831  mapsnen  7979  map1  7980  xpsnen  7988  xpcomco  7994  elfi2  8264  supmo  8302  infmo  8345  cp  8698  dfac5lem1  8890  dfac5lem2  8891  dfac5lem3  8892  dfac2  8897  kmlem3  8918  cdacomen  8947  cf0  9017  cflim3  9028  brdom7disj  9297  brdom6disj  9298  recmulnq  9730  letri3  10067  lesub0  10489  wloglei  10504  mulsuble0b  10839  creur  10958  indstr  11700  xrltlen  11923  xrletri3  11929  qbtwnre  11973  xmulcom  12039  xmulneg1  12042  xmulf  12045  iooneg  12234  iccneg  12235  elfzuzb  12278  fzrev  12345  ssfzoulel  12503  injresinj  12529  xpcogend  13647  rediv  13805  imdiv  13812  lenegsq  13994  o1lo1  14202  fsumcom2  14433  fsumcom2OLD  14434  fsumcom  14435  fprodcom2  14639  fprodcom2OLD  14640  fprodcom  14641  divalglem10  15049  smueqlem  15136  gcdcom  15159  dfgcd2  15187  lcmcom  15230  isprm2  15319  isprm7  15344  infpn2  15541  imasleval  16122  invsym  16343  dfiso3  16354  subsubc  16434  isffth2  16497  odulatb  17064  oduclatb  17065  posglbmo  17068  resscntz  17685  oppgid  17707  gsumcom  18297  dfrhm2  18638  lsslss  18880  fiidomfld  19227  opsrtoslem1  19403  xrsdsreclb  19712  znleval  19822  gsumcom3  20124  madutpos  20367  fvmptnn04if  20573  ntreq0  20791  restopn2  20891  ist0-3  21059  1stcelcls  21174  txkgen  21365  trfil2  21601  elflim2  21678  flimrest  21697  txflf  21720  fclsrest  21738  tsmssubm  21856  ismet2  22048  blres  22146  metrest  22239  restmetu  22285  xrtgioo  22517  elii1  22642  isclmp  22805  isncvsngp  22857  evthicc2  23136  ovolfcl  23142  ovoliunlem1  23177  dyaddisj  23270  mbfaddlem  23333  itg1climres  23387  mbfi1fseqlem4  23391  iblpos  23465  itgposval  23468  ditgsplit  23531  ellimc3  23549  itgsubst  23716  deg1ldg  23756  sincosq1sgn  24154  sincosq3sgn  24156  cos11  24183  dvdsflsumcom  24814  fsumvma  24838  logfaclbnd  24847  dchrelbas3  24863  lgsdi  24959  lgsquadlem1  25005  lgsquadlem2  25006  lgsquadlem3  25007  2lgslem1a  25016  istrkg2ld  25259  tgcgr4  25326  mirreu3  25449  hpgcom  25559  colhp  25562  dfcgra2  25621  nbgrel  26125  nbgrsym  26152  wlkson  26421  isspthonpth  26514  usgr2pth0  26530  wwlksnextinj  26663  elwspths2spth  26729  rusgrnumwwlkl1  26730  clwwlksn2  26776  0clwlk  26857  iseupthf1o  26928  eupth2lem2  26945  frgr2wwlk1  27052  fusgreg2wsp  27058  numclwwlkovf2  27073  frgrreg  27106  frgrregord013  27107  h2hcau  27685  h2hlm  27686  axhcompl-zf  27704  nmopub  28616  nmfnleub  28633  chrelati  29072  cvexchlem  29076  mdsymlem8  29118  sumdmdii  29123  spc2ed  29161  reuxfr3d  29178  rmo3f  29184  rmo4fOLD  29185  2ndpreima  29328  fpwrelmapffslem  29350  xrofsup  29377  pmtrprfv2  29633  smatrcl  29644  cnvordtrestixx  29741  issgon  29967  eulerpartlemr  30217  eulerpartlemgvv  30219  ballotlem2  30331  sgn3da  30384  bnj257  30480  bnj545  30673  bnj594  30690  coep  31349  dfpo2  31353  dfdm5  31378  dfrn5  31379  elima4  31381  frind  31441  nocvxmin  31554  brtxp  31629  elfix  31652  dffix2  31654  sscoid  31662  brimg  31686  brsuccf  31690  funpartfun  31692  dfrecs2  31699  dfrdg4  31700  cgrcomlr  31747  ofscom  31756  btwnexch  31774  fscgr  31829  bj-dfifc2  32206  bj-restuni  32687  bj-dfmpt2a  32708  bj-eldiag  32724  bj-ccinftydisj  32733  mptsnunlem  32817  topdifinffinlem  32827  wl-cases2-dnf  32927  wl-ax11-lem4  32997  fin2solem  33027  poimirlem4  33045  poimirlem26  33067  poimirlem30  33071  poimirlem32  33073  ftc1anclem6  33122  ftc1anc  33125  heibor1  33241  isdrngo3  33390  isdmn3  33505  prtlem70  33619  lrelat  33781  islshpat  33784  atlrelat1  34088  ishlat2  34120  pmapglb  34536  polval2N  34672  cdlemb3  35374  diblsmopel  35940  dicelval3  35949  diclspsn  35963  fz1eqin  36812  diophrex  36819  fphpd  36860  fzneg  37029  expdioph  37070  dford4  37076  lnr2i  37167  fgraphopab  37269  ifpancor  37289  ifpdfbi  37299  ifpidg  37317  ifpid2g  37319  ifpid1g  37320  ifpim23g  37321  ifp1bi  37328  rp-fakeoranass  37340  dfid7  37400  dfrtrcl5  37417  relexp0eq  37474  fsovrfovd  37785  rcompleq  37800  uunT1p1  38490  uun132p1  38495  un2122  38499  uun2131p1  38501  uunT12p1  38509  uunT12p2  38510  uunT12p3  38511  uun2221  38522  uun2221p1  38523  uun2221p2  38524  3impdirp1  38525  ancomstVD  38584  mapsnend  38865  icccncfext  39404  dvnmul  39464  dvmptfprodlem  39465  dvnprodlem2  39468  fourierdlem42  39673  fourierdlem83  39713  2reu3  40492  2reu7  40495  2reu8  40496  ndmaovcom  40589  sprvalpwn0  41021  2zrngnmrid  41238  opeliun2xp  41399  eliunxp2  41400
  Copyright terms: Public domain W3C validator