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  1401  nf4  1891  19.31  1897  r19.30  2845  eueq2  3100  uncom  3483  reuun2  3616  dfif2  3733  tppreqb  3931  ssunsn2  3950  prel12  3967  disjor  4188  zfpair  4393  ordtri2  4608  on0eqel  4690  somin1  5261  fununi  5508  swoer  6924  cantnflem1d  7633  cantnflem1  7634  cflim2  8132  dffin7-2  8267  fpwwe2lem13  8506  suplem2pr  8919  leloe  9150  fimaxre  9944  arch  10207  elznn0nn  10284  elznn0  10285  nneo  10342  ltxr  10704  xrleloe  10726  xrrebnd  10745  xmullem2  10833  xmulcom  10834  xmulneg1  10837  xmulf  10840  sqeqori  11481  hashtpg  11679  odd2np1lem  12895  dvdsprime  13080  coprm  13088  lvecvscan2  16172  opprdomn  16349  mplcoe1  16516  mplcoe2  16518  restntr  17234  alexsubALTlem2  18067  alexsubALTlem3  18068  xrsxmet  18828  dyaddisj  19476  mdegleb  19975  atandm3  20706  wilthlem2  20840  lgsdir2lem4  21098  nb3graprlem2  21449  eupath2lem2  21688  eupath2lem3  21689  hvmulcan2  22563  elat2  23831  chrelat2i  23856  atoml2i  23874  or3dir  23940  disjorf  24009  disjex  24020  disjexc  24021  funcnv5mpt  24072  elicoelioo  24129  xrdifh  24131  ofldsqr  24228  ballotlemfc0  24738  ballotlemfcc  24739  subfacp1lem6  24859  3orel2  25153  mulcan2g  25178  dfon2lem5  25398  axcontlem7  25857  btwnconn1lem14  25982  outsideofcom  26010  outsideofeu  26013  lineunray  26029  itg2addnclem2  26203  itgaddnclem2  26210  ecase13d  26253  elicc3  26257  nn0prpw  26263  stoweidlem26  27689  2reu3  27880  bnj563  28965  leatb  29929  leat2  29931  isat3  29944  hlrelat2  30039  elpadd0  30445
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