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

Theorem orcom 377
Description: Commutative law for disjunction. Theorem *4.31 of [WhiteheadRussell] p. 118. (Contributed by NM, 5-Aug-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 376 . 2  |-  ( (
ph  \/  ps )  ->  ( ps  \/  ph ) )
2 pm1.4 376 . 2  |-  ( ( ps  \/  ph )  ->  ( ph  \/  ps ) )
31, 2impbii 181 1  |-  ( (
ph  \/  ps )  <->  ( ps  \/  ph )
)
Colors of variables: wff set class
Syntax hints:    <-> wb 177    \/ wo 358
This theorem is referenced by:  orcomd  378  orbi1i  507  orass  511  or32  514  or42  516  orbi1d  684  pm5.61  694  oranabs  830  ordir  836  pm5.17  859  pm5.7  901  pm5.75  904  dn1  933  3orrot  942  3orcomb  946  cadan  1398  nf4  1887  19.31  1893  r19.30  2813  eueq2  3068  uncom  3451  reuun2  3584  dfif2  3701  tppreqb  3899  ssunsn2  3918  prel12  3935  disjor  4156  zfpair  4361  ordtri2  4576  on0eqel  4658  somin1  5229  fununi  5476  swoer  6892  cantnflem1d  7600  cantnflem1  7601  cflim2  8099  dffin7-2  8234  fpwwe2lem13  8473  suplem2pr  8886  leloe  9117  fimaxre  9911  arch  10174  elznn0nn  10251  elznn0  10252  nneo  10309  ltxr  10671  xrleloe  10693  xrrebnd  10712  xmullem2  10800  xmulcom  10801  xmulneg1  10804  xmulf  10807  sqeqori  11448  hashtpg  11646  odd2np1lem  12862  dvdsprime  13047  coprm  13055  lvecvscan2  16139  opprdomn  16316  mplcoe1  16483  mplcoe2  16485  restntr  17200  alexsubALTlem2  18032  alexsubALTlem3  18033  xrsxmet  18793  dyaddisj  19441  mdegleb  19940  atandm3  20671  wilthlem2  20805  lgsdir2lem4  21063  nb3graprlem2  21414  eupath2lem2  21653  eupath2lem3  21654  hvmulcan2  22528  elat2  23796  chrelat2i  23821  atoml2i  23839  or3dir  23905  disjorf  23974  disjex  23985  disjexc  23986  funcnv5mpt  24037  elicoelioo  24094  xrdifh  24096  ofldsqr  24193  ballotlemfc0  24703  ballotlemfcc  24704  subfacp1lem6  24824  3orel2  25118  mulcan2g  25143  dfon2lem5  25357  axcontlem7  25813  btwnconn1lem14  25938  outsideofcom  25966  outsideofeu  25969  lineunray  25985  itg2addnclem2  26156  itgaddnclem2  26163  ecase13d  26206  elicc3  26210  nn0prpw  26216  stoweidlem26  27642  2reu3  27833  bnj563  28817  leatb  29775  leat2  29777  isat3  29790  hlrelat2  29885  elpadd0  30291
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-or 360
  Copyright terms: Public domain W3C validator