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  664  pm5.32ri  671  pm5.32rd  673  anbi2ci  732  anbi12ci  734  an12  855  an32  856  an13  857  an42  883  andir  930  cases2  1016  dfbi3OLD  1019  dfifp6  1038  3anrot  1060  3ancoma  1062  nancom  1490  excxor  1509  cador  1587  cadcoma  1591  exancom  1827  19.42v  1921  19.42  2143  sbel2x  2487  moanmo  2561  2eu3  2584  2eu7  2588  2eu8  2589  eq2tri  2712  r19.28v  3100  r19.29r  3102  r19.42v  3121  rexcomf  3126  rabswap  3151  euxfr2  3424  rmo4  3432  reu8  3435  rmo3  3561  incom  3838  difin2  3923  euelss  3947  ssunsn  4392  inuni  4856  reuxfr2d  4921  eqvinop  4984  dfid3  5054  elxp2  5166  elvvv  5212  brinxp2  5214  dmuni  5366  dfres2  5488  restidsing  5493  dfima2  5503  imadmrn  5511  imai  5513  asymref2  5548  cnvxp  5586  xpdifid  5597  cnvcnvsn  5648  opswap  5660  mptpreima  5666  rnco  5679  ressn  5709  xpco  5713  wfi  5751  elon2  5772  fncnv  6000  fununi  6002  fnres  6045  mptfnf  6053  fnopabg  6055  dff1o2  6180  eqfnfv3  6353  respreima  6384  fsn  6442  f13dfv  6570  fliftcnv  6601  isoini  6628  elrnmpt2res  6816  ndmovcom  6863  uniuni  7013  mptmpt2opabbrd  7293  brtpos2  7403  brtpos  7406  tpostpos  7417  tposmpt2  7434  mpt2curryd  7440  oaord  7672  oeeu  7728  nnaord  7744  pmex  7904  elpmg  7915  mapval2  7929  mapsnen  8076  map1  8077  xpsnen  8085  xpcomco  8091  elfi2  8361  supmo  8399  infmo  8442  cp  8792  dfac5lem1  8984  dfac5lem2  8985  dfac5lem3  8986  dfac2  8991  kmlem3  9012  cdacomen  9041  cf0  9111  cflim3  9122  brdom7disj  9391  brdom6disj  9392  recmulnq  9824  letri3  10161  lesub0  10583  wloglei  10598  mulsuble0b  10933  creur  11052  indstr  11794  xrltlen  12017  xrletri3  12023  qbtwnre  12068  xmulcom  12134  xmulneg1  12137  xmulf  12140  iooneg  12330  iccneg  12331  elfzuzb  12374  fzrev  12441  ssfzoulel  12602  injresinj  12629  xpcogend  13759  rediv  13915  imdiv  13922  lenegsq  14104  o1lo1  14312  fsumcom2  14549  fsumcom2OLD  14550  fsumcom  14551  fprodcom2  14758  fprodcom2OLD  14759  fprodcom  14760  divalglem10  15172  smueqlem  15259  gcdcom  15282  dfgcd2  15310  lcmcom  15353  isprm2  15442  isprm7  15467  infpn2  15664  imasleval  16248  invsym  16469  dfiso3  16480  subsubc  16560  isffth2  16623  odulatb  17190  oduclatb  17191  posglbmo  17194  resscntz  17810  oppgid  17832  gsumcom  18422  dfrhm2  18765  lsslss  19009  fiidomfld  19356  opsrtoslem1  19532  xrsdsreclb  19841  znleval  19951  gsumcom3  20253  madutpos  20496  fvmptnn04if  20702  ntreq0  20929  restopn2  21029  ist0-3  21197  1stcelcls  21312  txkgen  21503  trfil2  21738  elflim2  21815  flimrest  21834  txflf  21857  fclsrest  21875  tsmssubm  21993  ismet2  22185  blres  22283  metrest  22376  restmetu  22422  xrtgioo  22656  elii1  22781  isclmp  22943  isncvsngp  22995  evthicc2  23275  ovolfcl  23281  ovoliunlem1  23316  dyaddisj  23410  mbfaddlem  23472  itg1climres  23526  mbfi1fseqlem4  23530  iblpos  23604  itgposval  23607  ditgsplit  23670  ellimc3  23688  itgsubst  23857  deg1ldg  23897  sincosq1sgn  24295  sincosq3sgn  24297  cos11  24324  dvdsflsumcom  24959  fsumvma  24983  logfaclbnd  24992  dchrelbas3  25008  lgsdi  25104  lgsquadlem1  25150  lgsquadlem2  25151  lgsquadlem3  25152  2lgslem1a  25161  istrkg2ld  25404  tgcgr4  25471  mirreu3  25594  hpgcom  25704  colhp  25707  dfcgra2  25766  nbgrel  26278  nbgrelOLD  26279  nbgrsym  26308  nbgrsymOLD  26309  wlkson  26608  isspthonpth  26701  usgr2pth0  26717  wwlksnextinj  26862  elwspths2spth  26934  rusgrnumwwlkl1  26935  clwwlknclwwlkdifnum  26946  clwwlkn1  27004  clwwlkn2  27007  0clwlk  27108  iseupthf1o  27180  eupth2lem2  27197  frgrncvvdeqlem2  27280  fusgr2wsp2nb  27314  fusgreg2wsp  27316  numclwwlkqhash  27355  frgrreg  27381  frgrregord013  27382  h2hcau  27964  h2hlm  27965  axhcompl-zf  27983  nmopub  28895  nmfnleub  28912  chrelati  29351  cvexchlem  29355  mdsymlem8  29397  sumdmdii  29402  spc2ed  29440  reuxfr3d  29456  rmo3f  29462  rmo4fOLD  29463  difrab2  29465  2ndpreima  29613  fpwrelmapffslem  29635  xrofsup  29661  pmtrprfv2  29976  smatrcl  29990  cnvordtrestixx  30087  issgon  30314  eulerpartlemr  30564  eulerpartlemgvv  30566  ballotlem2  30678  sgn3da  30731  oddprm2  30861  bnj257  30901  bnj545  31091  bnj594  31108  coep  31767  dfpo2  31771  dfdm5  31800  dfrn5  31801  elima4  31803  frpoind  31865  frind  31868  sletri3  32005  nocvxmin  32019  sltrec  32049  brtxp  32112  elfix  32135  dffix2  32137  sscoid  32145  brimg  32169  brsuccf  32173  funpartfun  32175  dfrecs2  32182  dfrdg4  32183  cgrcomlr  32230  ofscom  32239  btwnexch  32257  fscgr  32312  bj-dfifc2  32689  bj-restuni  33175  bj-0int  33180  bj-dfmpt2a  33196  bj-eldiag  33221  bj-ccinftydisj  33230  mptsnunlem  33315  topdifinffinlem  33325  wl-cases2-dnf  33425  wl-ax11-lem4  33495  fin2solem  33525  poimirlem4  33543  poimirlem26  33565  poimirlem30  33569  poimirlem32  33571  ftc1anclem6  33620  ftc1anc  33623  heibor1  33739  isdrngo3  33888  isdmn3  34003  biancom  34137  biancomd  34138  an2anr  34141  anan  34142  brinxp2ALTV  34175  inxpxrn  34293  prtlem70  34460  lrelat  34619  islshpat  34622  atlrelat1  34926  ishlat2  34958  pmapglb  35374  polval2N  35510  cdlemb3  36211  diblsmopel  36777  dicelval3  36786  diclspsn  36800  fz1eqin  37649  diophrex  37656  fphpd  37697  fzneg  37866  expdioph  37907  dford4  37913  lnr2i  38003  fgraphopab  38105  ifpancor  38125  ifpdfbi  38135  ifpidg  38153  ifpid2g  38155  ifpid1g  38156  ifpim23g  38157  ifp1bi  38164  rp-fakeoranass  38176  dfid7  38236  dfrtrcl5  38253  relexp0eq  38310  fsovrfovd  38620  rcompleq  38635  uunT1p1  39325  uun132p1  39330  un2122  39334  uun2131p1  39336  uunT12p1  39344  uunT12p2  39345  uunT12p3  39346  uun2221  39357  uun2221p1  39358  uun2221p2  39359  3impdirp1  39360  ancomstVD  39415  mapsnend  39705  icccncfext  40418  dvnmul  40476  dvmptfprodlem  40477  dvnprodlem2  40480  fourierdlem42  40684  fourierdlem83  40724  2reu3  41509  2reu7  41512  2reu8  41513  ndmaovcom  41606  an4com24  41609  4an21  41611  sprvalpwn0  42058  2zrngnmrid  42275  opeliun2xp  42436  eliunxp2  42437
  Copyright terms: Public domain W3C validator