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

Theorem orcom 387
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 386 . 2  |-  ( (
ph  \/  ps )  ->  ( ps  \/  ph ) )
2 pm1.4 386 . 2  |-  ( ( ps  \/  ph )  ->  ( ph  \/  ps ) )
31, 2impbii 188 1  |-  ( (
ph  \/  ps )  <->  ( ps  \/  ph )
)
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    \/ wo 368
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 185  df-or 370
This theorem is referenced by:  orcomd  388  orbi1i  517  orass  521  or32  524  or42  526  orbi1d  697  pm5.61  707  oranabs  847  ordir  855  pm5.17  878  pm5.7  920  pm5.75  923  dn1  952  3orrot  966  3orcomb  970  cadan  1438  cadanOLD  1439  thema1a  1584  nf4  1894  19.31  1900  r19.30  2863  eueq2  3130  uncom  3497  reuun2  3630  dfif2  3790  rabrsn  3942  tppreqb  4011  ssunsn2  4029  prel12  4046  disjor  4273  zfpair  4526  ordtri2  4750  on0eqel  4832  somin1  5231  fununi  5481  eliman0  5716  swoer  7125  cantnflem1d  7892  cantnflem1  7893  cantnflem1dOLD  7915  cantnflem1OLD  7916  cflim2  8428  dffin7-2  8563  fpwwe2lem13  8805  suplem2pr  9218  leloe  9457  mulcan2g  9986  fimaxre  10273  arch  10572  elznn0nn  10656  elznn0  10657  nneo  10721  ltxr  11091  xrleloe  11117  xrrebnd  11136  xmullem2  11224  xmulcom  11225  xmulneg1  11228  xmulf  11231  sqeqori  11974  hashtpg  12182  odd2np1lem  13587  dvdsprime  13772  coprm  13782  lvecvscan2  17171  opprdomn  17351  mplcoe1  17522  mplcoe2  17525  mplcoe2OLD  17526  madutpos  18407  restntr  18745  alexsubALTlem2  19579  alexsubALTlem3  19580  xrsxmet  20345  dyaddisj  21035  mdegleb  21494  atandm3  22232  wilthlem2  22366  lgsdir2lem4  22624  tgcolg  22946  axcontlem7  23151  nb3graprlem2  23295  eupath2lem2  23534  eupath2lem3  23535  hvmulcan2  24410  elat2  25679  chrelat2i  25704  atoml2i  25722  or3dir  25788  disjnf  25851  disjorf  25858  disjex  25869  disjexc  25870  disjunsn  25871  funcnv5mpt  25923  elicoelioo  26001  xrdifh  26003  tlt3  26059  orngsqr  26207  ballotlemfc0  26805  ballotlemfcc  26806  subfacp1lem6  27003  3orel2  27296  socnv  27504  dfon2lem5  27529  btwnconn1lem14  28060  outsideofcom  28088  outsideofeu  28091  lineunray  28107  itg2addnclem2  28369  itgaddnclem2  28376  ecase13d  28433  elicc3  28437  nn0prpw  28443  orfa  28807  unitresl  28810  notornotel2  28824  tsbi4  28872  stoweidlem26  29746  2reu3  29937  bnj563  31569  bj-nf2  31927  bj-nfn  31954  leatb  32659  leat2  32661  isat3  32674  hlrelat2  32769  elpadd0  33175
  Copyright terms: Public domain W3C validator