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

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
StepHypRef Expression
1 pm3.22 464 . 2 ((𝜑𝜓) → (𝜓𝜑))
2 pm3.22 464 . 2 ((𝜓𝜑) → (𝜑𝜓))
31, 2impbii 199 1 ((𝜑𝜓) ↔ (𝜓𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 383
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 385
This theorem is referenced by:  ancomd  466  ancomst  467  ancomsd  469  pm4.71r  666  pm5.32ri  673  pm5.32rd  675  anbi2ci  734  anbi12ci  736  an12  873  an32  874  an13  875  an42  901  andir  948  cases2  1034  dfbi3OLD  1037  dfifp6  1056  3ancomaOLD  1085  3anrotOLD  1089  nancom  1599  excxor  1618  cador  1696  cadcoma  1700  exancom  1936  19.42v  2030  19.42  2252  sbel2x  2596  moanmo  2670  2eu3  2693  2eu7  2697  2eu8  2698  eq2tri  2821  r19.28v  3209  r19.29r  3211  r19.42v  3230  rexcomf  3235  rabswap  3260  euxfr2  3532  rmo4  3540  reu8  3543  rmo3  3669  incom  3948  difin2  4033  euelss  4057  ssunsn  4505  inuni  4975  reuxfr2d  5040  eqvinop  5103  dfid3  5175  elxp2  5289  elvvv  5335  brinxp2  5337  dmuni  5489  dfres2  5611  restidsing  5616  dfima2  5626  imadmrn  5634  imai  5636  asymref2  5671  cnvxp  5709  xpdifid  5720  cnvcnvsn  5771  opswap  5783  mptpreima  5789  rnco  5802  ressn  5832  xpco  5836  wfi  5874  elon2  5895  fncnv  6123  fununi  6125  fnres  6168  mptfnf  6176  fnopabg  6178  dff1o2  6303  eqfnfv3  6476  respreima  6507  fsn  6565  f13dfv  6693  fliftcnv  6724  isoini  6751  elrnmpt2res  6939  ndmovcom  6986  uniuni  7136  mptmpt2opabbrd  7416  brtpos2  7527  brtpos  7530  tpostpos  7541  tposmpt2  7558  mpt2curryd  7564  oaord  7796  oeeu  7852  nnaord  7868  pmex  8028  elpmg  8039  mapval2  8053  mapsnen  8200  map1  8201  xpsnen  8209  xpcomco  8215  elfi2  8485  supmo  8523  infmo  8566  cp  8927  dfac5lem1  9136  dfac5lem2  9137  dfac5lem3  9138  dfac2b  9143  dfac2OLD  9145  kmlem3  9166  cdacomen  9195  cf0  9265  cflim3  9276  brdom7disj  9545  brdom6disj  9546  recmulnq  9978  letri3  10315  lesub0  10737  wloglei  10752  mulsuble0b  11087  creur  11206  indstr  11949  xrltlen  12172  xrletri3  12178  qbtwnre  12223  xmulcom  12289  xmulneg1  12292  xmulf  12295  iooneg  12485  iccneg  12486  elfzuzb  12529  fzrev  12596  ssfzoulel  12756  injresinj  12783  xpcogend  13914  rediv  14070  imdiv  14077  lenegsq  14259  o1lo1  14467  fsumcom2  14704  fsumcom2OLD  14705  fsumcom  14706  fprodcom2  14913  fprodcom2OLD  14914  fprodcom  14915  divalglem10  15327  smueqlem  15414  gcdcom  15437  dfgcd2  15465  lcmcom  15508  isprm2  15597  isprm7  15622  infpn2  15819  imasleval  16403  invsym  16623  dfiso3  16634  subsubc  16714  isffth2  16777  odulatb  17344  oduclatb  17345  posglbmo  17348  resscntz  17964  oppgid  17986  gsumcom  18576  dfrhm2  18919  lsslss  19163  fiidomfld  19510  opsrtoslem1  19686  xrsdsreclb  19995  znleval  20105  gsumcom3  20407  madutpos  20650  fvmptnn04if  20856  ntreq0  21083  restopn2  21183  ist0-3  21351  1stcelcls  21466  txkgen  21657  trfil2  21892  elflim2  21969  flimrest  21988  txflf  22011  fclsrest  22029  tsmssubm  22147  ismet2  22339  blres  22437  metrest  22530  restmetu  22576  xrtgioo  22810  elii1  22935  isclmp  23097  isncvsngp  23149  evthicc2  23429  ovolfcl  23435  ovoliunlem1  23470  dyaddisj  23564  mbfaddlem  23626  itg1climres  23680  mbfi1fseqlem4  23684  iblpos  23758  itgposval  23761  ditgsplit  23824  ellimc3  23842  itgsubst  24011  deg1ldg  24051  sincosq1sgn  24449  sincosq3sgn  24451  cos11  24478  dvdsflsumcom  25113  fsumvma  25137  logfaclbnd  25146  dchrelbas3  25162  lgsdi  25258  lgsquadlem1  25304  lgsquadlem2  25305  lgsquadlem3  25306  2lgslem1a  25315  istrkg2ld  25558  tgcgr4  25625  mirreu3  25748  hpgcom  25858  colhp  25861  dfcgra2  25920  nbgrel  26432  nbgrelOLD  26433  nbgrsym  26462  nbgrsymOLD  26463  wlkson  26762  isspthonpth  26855  usgr2pth0  26871  wwlksnextinj  27017  elwspths2spth  27089  rusgrnumwwlkl1  27090  clwwlknclwwlkdifnum  27101  clwwlkn1  27170  clwwlkn2  27173  0clwlk  27282  iseupthf1o  27354  eupth2lem2  27371  frgrncvvdeqlem2  27454  fusgr2wsp2nb  27488  fusgreg2wsp  27490  numclwwlkqhash  27536  frgrreg  27562  frgrregord013  27563  h2hcau  28145  h2hlm  28146  axhcompl-zf  28164  nmopub  29076  nmfnleub  29093  chrelati  29532  cvexchlem  29536  mdsymlem8  29578  sumdmdii  29583  spc2ed  29621  reuxfr3d  29637  rmo3f  29643  rmo4fOLD  29644  difrab2  29646  2ndpreima  29794  fpwrelmapffslem  29816  xrofsup  29842  pmtrprfv2  30157  smatrcl  30171  cnvordtrestixx  30268  issgon  30495  eulerpartlemr  30745  eulerpartlemgvv  30747  ballotlem2  30859  sgn3da  30912  oddprm2  31042  bnj257  31082  bnj545  31272  bnj594  31289  coep  31948  dfpo2  31952  dfdm5  31981  dfrn5  31982  elima4  31984  frpoind  32046  frind  32049  sletri3  32186  nocvxmin  32200  sltrec  32230  brtxp  32293  elfix  32316  dffix2  32318  sscoid  32326  brimg  32350  brsuccf  32354  funpartfun  32356  dfrecs2  32363  dfrdg4  32364  cgrcomlr  32411  ofscom  32420  btwnexch  32438  fscgr  32493  bj-dfifc2  32870  bj-restuni  33356  bj-0int  33361  bj-dfmpt2a  33377  bj-eldiag  33402  bj-ccinftydisj  33411  mptsnunlem  33496  topdifinffinlem  33506  wl-cases2-dnf  33608  wl-ax11-lem4  33678  fin2solem  33708  poimirlem4  33726  poimirlem26  33748  poimirlem30  33752  poimirlem32  33754  ftc1anclem6  33803  ftc1anc  33806  heibor1  33922  isdrngo3  34071  isdmn3  34186  biancom  34320  biancomd  34321  an2anr  34324  anan  34325  brinxp2ALTV  34358  inxpxrn  34476  prtlem70  34645  lrelat  34804  islshpat  34807  atlrelat1  35111  ishlat2  35143  pmapglb  35559  polval2N  35695  cdlemb3  36396  diblsmopel  36962  dicelval3  36971  diclspsn  36985  fz1eqin  37834  diophrex  37841  fphpd  37882  fzneg  38051  expdioph  38092  dford4  38098  lnr2i  38188  fgraphopab  38290  ifpancor  38310  ifpdfbi  38320  ifpidg  38338  ifpid2g  38340  ifpid1g  38341  ifpim23g  38342  ifp1bi  38349  rp-fakeoranass  38361  dfid7  38421  dfrtrcl5  38438  relexp0eq  38495  fsovrfovd  38805  rcompleq  38820  uunT1p1  39510  uun132p1  39515  un2122  39519  uun2131p1  39521  uunT12p1  39529  uunT12p2  39530  uunT12p3  39531  uun2221  39542  uun2221p1  39543  uun2221p2  39544  3impdirp1  39545  ancomstVD  39600  mapsnend  39890  icccncfext  40603  dvnmul  40661  dvmptfprodlem  40662  dvnprodlem2  40665  fourierdlem42  40869  fourierdlem83  40909  2reu3  41694  2reu7  41697  2reu8  41698  ndmaovcom  41791  an4com24  41794  4an21  41796  sprvalpwn0  42243  2zrngnmrid  42460  opeliun2xp  42621  eliunxp2  42622
  Copyright terms: Public domain W3C validator