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

Theorem orcom 389
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  |-  ( (
ph  \/  ps )  <->  ( ps  \/  ph )
)

Proof of Theorem orcom
StepHypRef Expression
1 pm1.4 388 . 2  |-  ( (
ph  \/  ps )  ->  ( ps  \/  ph ) )
2 pm1.4 388 . 2  |-  ( ( ps  \/  ph )  ->  ( ph  \/  ps ) )
31, 2impbii 191 1  |-  ( (
ph  \/  ps )  <->  ( ps  \/  ph )
)
Colors of variables: wff setvar class
Syntax hints:    <-> wb 188    \/ wo 370
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 189  df-or 372
This theorem is referenced by:  orcomd  390  orbi1i  523  orass  527  or32  530  or42  532  orbi1d  708  pm5.61  718  oranabs  865  ordir  874  pm5.17  897  pm5.7  943  pm5.75  946  dn1  975  3orrot  989  3orcomb  993  dfifp7  1428  cadan  1508  cadcomb  1512  stoic1aOLD  1653  19.31v  1780  nf4  2019  19.31  2024  r19.30  2974  eueq2  3246  uncom  3611  reuun2  3757  dfif2  3912  rabrsn  4068  tppreqb  4139  ssunsn2  4157  prel12  4175  disjor  4406  zfpair  4656  somin1  5250  ordtri2  5475  on0eqel  5557  fununi  5665  eliman0  5908  swoer  7397  supgtoreq  7990  cantnflem1d  8196  cantnflem1  8197  cflim2  8695  dffin7-2  8830  fpwwe2lem13  9069  suplem2pr  9480  leloe  9722  mulcan2g  10268  fimaxre  10553  arch  10868  elznn0nn  10953  elznn0  10954  nneo  11021  ltxr  11417  xrleloe  11445  xrrebnd  11465  xmullem2  11553  xmulcom  11554  xmulneg1  11557  xmulf  11560  sqeqori  12387  hashtpg  12639  odd2np1lem  14357  lcmcom  14550  dvdsprime  14630  coprm  14650  lvecvscan2  18328  opprdomn  18518  mplcoe1  18682  mplcoe5  18685  madutpos  19659  restntr  20190  alexsubALTlem2  21055  alexsubALTlem3  21056  xrsxmet  21819  dyaddisj  22546  mdegleb  23005  atandm3  23796  wilthlem2  23986  lgsdir2lem4  24246  tgcolg  24591  hlcomb  24640  axcontlem7  24992  nb3graprlem2  25172  eupath2lem2  25698  eupath2lem3  25699  hvmulcan2  26718  elat2  27985  chrelat2i  28010  atoml2i  28028  or3dir  28094  disjnf  28177  disjorf  28185  disjex  28198  disjexc  28199  disjunsn  28200  funcnv5mpt  28268  elicoelioo  28360  xrdifh  28362  tlt3  28427  orngsqr  28569  ballotlemfc0  29327  ballotlemfcc  29328  bnj563  29555  subfacp1lem6  29910  3orel2  30345  socnv  30406  dfon2lem5  30434  btwnconn1lem14  30866  outsideofcom  30894  outsideofeu  30897  lineunray  30913  ecase13d  30968  elicc3  30972  nn0prpw  30978  bj-dfbi5  31149  bj-consensusALT  31156  bj-nf2  31189  bj-nfn  31212  topdifinfeq  31711  onsucuni3  31728  wl-cases2-dnf  31808  itg2addnclem2  31952  itgaddnclem2  31959  orfa  32273  unitresl  32276  notornotel2  32290  tsbi4  32336  leatb  32821  leat2  32823  isat3  32836  hlrelat2  32931  elpadd0  33337  ifporcor  36069  ifpim2  36079  ifpim23g  36103  ifpim123g  36108  rp-fakeoranass  36122  elprn2  37578  stoweidlem26  37750  2reu3  38366
  Copyright terms: Public domain W3C validator