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  854  ordir  863  pm5.17  886  pm5.7  932  pm5.75  935  dn1  964  3orrot  979  3orcomb  983  cadan  1443  cadanOLD  1444  thema1a  1589  nf4  1911  19.31  1917  r19.30  3006  eueq2  3277  uncom  3648  reuun2  3781  dfif2  3941  rabrsn  4097  tppreqb  4168  ssunsn2  4186  prel12  4203  disjor  4431  zfpair  4684  ordtri2  4913  on0eqel  4995  somin1  5402  fununi  5653  eliman0  5894  swoer  7339  supgtoreq  7927  cantnflem1d  8106  cantnflem1  8107  cantnflem1dOLD  8129  cantnflem1OLD  8130  cflim2  8642  dffin7-2  8777  fpwwe2lem13  9019  suplem2pr  9430  leloe  9670  mulcan2g  10202  fimaxre  10489  arch  10791  elznn0nn  10877  elznn0  10878  nneo  10943  ltxr  11323  xrleloe  11349  xrrebnd  11368  xmullem2  11456  xmulcom  11457  xmulneg1  11460  xmulf  11463  sqeqori  12247  hashtpg  12488  odd2np1lem  13903  dvdsprime  14088  coprm  14099  lvecvscan2  17553  opprdomn  17737  mplcoe1  17914  mplcoe5  17918  mplcoe2OLD  17920  madutpos  18927  restntr  19465  alexsubALTlem2  20299  alexsubALTlem3  20300  xrsxmet  21065  dyaddisj  21756  mdegleb  22215  atandm3  22953  wilthlem2  23087  lgsdir2lem4  23345  tgcolg  23685  axcontlem7  23965  nb3graprlem2  24144  eupath2lem2  24670  eupath2lem3  24671  hvmulcan2  25682  elat2  26951  chrelat2i  26976  atoml2i  26994  or3dir  27060  disjnf  27122  disjorf  27129  disjex  27140  disjexc  27141  disjunsn  27142  funcnv5mpt  27199  elicoelioo  27273  xrdifh  27275  tlt3  27331  orngsqr  27473  ballotlemfc0  28087  ballotlemfcc  28088  subfacp1lem6  28285  3orel2  28579  socnv  28787  dfon2lem5  28812  btwnconn1lem14  29343  outsideofcom  29371  outsideofeu  29374  lineunray  29390  itg2addnclem2  29660  itgaddnclem2  29667  ecase13d  29724  elicc3  29728  nn0prpw  29734  orfa  30098  unitresl  30101  notornotel2  30115  tsbi4  30163  lcmcom  30815  elunnel2  31009  elprn2  31192  stoweidlem26  31342  2reu3  31676  bnj563  32888  bj-dfbi5  33231  bj-dfif7  33241  bj-nf2  33288  bj-nfn  33316  leatb  34098  leat2  34100  isat3  34113  hlrelat2  34208  elpadd0  34614
  Copyright terms: Public domain W3C validator