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

Theorem orcom 864
Description: Commutative law for disjunction. Theorem *4.31 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 15-Nov-2012.)
Assertion
Ref Expression
orcom ((𝜑𝜓) ↔ (𝜓𝜑))

Proof of Theorem orcom
StepHypRef Expression
1 pm1.4 863 . 2 ((𝜑𝜓) → (𝜓𝜑))
2 pm1.4 863 . 2 ((𝜓𝜑) → (𝜑𝜓))
31, 2impbii 210 1 ((𝜑𝜓) ↔ (𝜓𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 207  wo 841
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 208  df-or 842
This theorem is referenced by:  orcomd  865  unitresl  866  orbi1i  907  orbi1d  910  orass  915  or32  919  or42  921  pm5.7  947  oranabs  993  ordir  1000  pm5.17  1005  dn1  1049  dfifp7  1061  3orrot  1084  norcom  1514  norass  1524  cadan  1601  cadcomb  1605  nf2  1777  nfnbi  1846  19.31v  1933  19.31  2227  r19.30OLD  3339  eueq2  3700  uncom  4128  undif3  4264  reuun2  4285  dfif2  4467  reuprg  4633  rabrsn  4654  tppreqb  4732  ssunsn2  4754  disjor  5038  zfpair  5313  somin1  5987  ordtri2  6220  on0eqel  6302  fununi  6423  eliman0  6699  swoer  8309  supgtoreq  8923  cantnflem1d  9140  cantnflem1  9141  cflim2  9674  dffin7-2  9809  fpwwe2lem13  10053  suplem2pr  10464  leloe  10716  mulcan2g  11283  fimaxre  11573  fimaxreOLD  11574  fiminre  11577  arch  11883  elznn0nn  11984  elznn0  11985  nneo  12055  ltxr  12500  xrleloe  12527  xrrebnd  12551  xmullem2  12648  xmulcom  12649  xmulneg1  12652  xmulf  12655  sqeqori  13566  hashtpg  13833  odd2np1lem  15679  lcmcom  15927  dvdsprime  16021  coprm  16045  lvecvscan2  19815  opprdomn  20004  mplcoe1  20176  mplcoe5  20179  madutpos  21181  restntr  21720  alexsubALTlem2  22586  alexsubALTlem3  22587  xrsxmet  23346  dyaddisj  24126  mdegleb  24587  atandm3  25383  wilthlem2  25574  lgsdir2lem4  25832  tgcolg  26268  hlcomb  26317  axcontlem7  26684  elntg2  26699  nb3grprlem2  27091  vtxd0nedgb  27198  clwwlkneq0  27735  eupth2lem2  27926  eupth2lem3lem6  27940  numclwwlk3lem2lem  28090  hvmulcan2  28778  elat2  30045  chrelat2i  30070  atoml2i  30088  or3dir  30154  rmounid  30187  disjnf  30249  disjorf  30258  disjex  30271  disjexc  30272  disjunsn  30273  funcnv5mpt  30342  elicoelioo  30428  xrdifh  30430  dvdszzq  30458  tlt3  30580  orngsqr  30805  ballotlemfc0  31650  ballotlemfcc  31651  bnj563  31914  subfacp1lem6  32330  3orel2  32839  dfon2lem5  32930  noextenddif  33073  sleloe  33131  btwnconn1lem14  33459  outsideofcom  33487  outsideofeu  33490  lineunray  33506  ecase13d  33559  elicc3  33563  nn0prpw  33569  bj-dfbi5  33805  bj-consensusALT  33810  topdifinfeq  34514  onsucuni3  34531  wl-cases2-dnf  34635  itg2addnclem2  34826  itgaddnclem2  34833  orfa  35243  notornotel2  35257  tsbi4  35297  ineleq  35491  leatb  36310  leat2  36312  isat3  36325  hlrelat2  36421  elpadd0  36827  ifporcor  39707  ifpim2  39717  ifpim23g  39741  ifpim123g  39746  rp-fakeoranass  39760  ontric3g  39768  elprn2  41795  stoweidlem26  42192  2reu3  43190  itschlc0xyqsol1  44651  itschlc0xyqsol  44652  inlinecirc02plem  44671
  Copyright terms: Public domain W3C validator