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, 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 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  520  orass  524  or32  527  or42  529  orbi1d  702  pm5.61  712  oranabs  852  ordir  860  pm5.17  883  pm5.7  925  pm5.75  928  dn1  957  3orrot  971  3orcomb  975  cadan  1433  cadanOLD  1434  thema1a  1579  nf4  1890  19.31  1896  r19.30  2877  eueq2  3145  uncom  3512  reuun2  3645  dfif2  3805  rabrsn  3957  tppreqb  4026  ssunsn2  4044  prel12  4061  disjor  4288  zfpair  4541  ordtri2  4766  on0eqel  4848  somin1  5246  fununi  5496  eliman0  5731  swoer  7141  cantnflem1d  7908  cantnflem1  7909  cantnflem1dOLD  7931  cantnflem1OLD  7932  cflim2  8444  dffin7-2  8579  fpwwe2lem13  8821  suplem2pr  9234  leloe  9473  mulcan2g  10002  fimaxre  10289  arch  10588  elznn0nn  10672  elznn0  10673  nneo  10737  ltxr  11107  xrleloe  11133  xrrebnd  11152  xmullem2  11240  xmulcom  11241  xmulneg1  11244  xmulf  11247  sqeqori  11990  hashtpg  12198  odd2np1lem  13603  dvdsprime  13788  coprm  13798  lvecvscan2  17205  opprdomn  17385  mplcoe1  17556  mplcoe5  17560  mplcoe2OLD  17562  madutpos  18460  restntr  18798  alexsubALTlem2  19632  alexsubALTlem3  19633  xrsxmet  20398  dyaddisj  21088  mdegleb  21547  atandm3  22285  wilthlem2  22419  lgsdir2lem4  22677  tgcolg  23000  axcontlem7  23228  nb3graprlem2  23372  eupath2lem2  23611  eupath2lem3  23612  hvmulcan2  24487  elat2  25756  chrelat2i  25781  atoml2i  25799  or3dir  25865  disjnf  25928  disjorf  25935  disjex  25946  disjexc  25947  disjunsn  25948  funcnv5mpt  26000  elicoelioo  26080  xrdifh  26082  tlt3  26138  orngsqr  26284  ballotlemfc0  26887  ballotlemfcc  26888  subfacp1lem6  27085  3orel2  27379  socnv  27587  dfon2lem5  27612  btwnconn1lem14  28143  outsideofcom  28171  outsideofeu  28174  lineunray  28190  itg2addnclem2  28456  itgaddnclem2  28463  ecase13d  28520  elicc3  28524  nn0prpw  28530  orfa  28894  unitresl  28897  notornotel2  28911  tsbi4  28959  stoweidlem26  29833  2reu3  30024  supgtoreq  30755  bnj563  31747  bj-dfbi5  32090  bj-dfif7  32100  bj-nf2  32145  bj-nfn  32173  leatb  32949  leat2  32951  isat3  32964  hlrelat2  33059  elpadd0  33465
  Copyright terms: Public domain W3C validator