MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  orcom 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

Proof of Theorem orcom
StepHypRef Expression
1 pm1.4 386 . 2
2 pm1.4 386 . 2
31, 2impbii 188 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  \/wo 368
This theorem is referenced by:  orcomd  388  orbi1i  520  orass  524  or32  527  or42  529  orbi1d  702  pm5.61  712  oranabs  856  ordir  865  pm5.17  888  pm5.7  934  pm5.75  937  dn1  966  3orrot  979  3orcomb  983  dfifp7  1387  cadan  1459  stoic1a  1605  19.31v  1731  nf4  1962  19.31  1968  r19.30  3002  eueq2  3273  uncom  3647  reuun2  3780  dfif2  3943  rabrsn  4100  tppreqb  4171  ssunsn2  4189  prel12  4207  disjor  4436  zfpair  4689  ordtri2  4918  on0eqel  5000  somin1  5408  fununi  5659  eliman0  5900  swoer  7358  supgtoreq  7949  cantnflem1d  8128  cantnflem1  8129  cantnflem1dOLD  8151  cantnflem1OLD  8152  cflim2  8664  dffin7-2  8799  fpwwe2lem13  9041  suplem2pr  9452  leloe  9692  mulcan2g  10228  fimaxre  10515  arch  10817  elznn0nn  10903  elznn0  10904  nneo  10971  ltxr  11353  xrleloe  11379  xrrebnd  11398  xmullem2  11486  xmulcom  11487  xmulneg1  11490  xmulf  11493  sqeqori  12280  hashtpg  12523  odd2np1lem  14045  dvdsprime  14230  coprm  14241  lvecvscan2  17758  opprdomn  17950  mplcoe1  18127  mplcoe5  18131  mplcoe2OLD  18133  madutpos  19144  restntr  19683  alexsubALTlem2  20548  alexsubALTlem3  20549  xrsxmet  21314  dyaddisj  22005  mdegleb  22464  atandm3  23209  wilthlem2  23343  lgsdir2lem4  23601  tgcolg  23941  hlcomb  23987  axcontlem7  24273  nb3graprlem2  24452  eupath2lem2  24978  eupath2lem3  24979  hvmulcan2  25990  elat2  27259  chrelat2i  27284  atoml2i  27302  or3dir  27368  disjnf  27433  disjorf  27440  disjex  27451  disjexc  27452  disjunsn  27453  funcnv5mpt  27511  elicoelioo  27589  xrdifh  27591  tlt3  27653  orngsqr  27794  ballotlemfc0  28431  ballotlemfcc  28432  subfacp1lem6  28629  3orel2  29088  socnv  29194  dfon2lem5  29219  btwnconn1lem14  29750  outsideofcom  29778  outsideofeu  29781  lineunray  29797  itg2addnclem2  30067  itgaddnclem2  30074  ecase13d  30131  elicc3  30135  nn0prpw  30141  orfa  30479  unitresl  30482  notornotel2  30496  tsbi4  30543  lcmcom  31199  elprn2  31640  stoweidlem26  31808  2reu3  32193  bnj563  33800  bj-dfbi5  34155  bj-nf2  34196  bj-nfn  34219  leatb  35017  leat2  35019  isat3  35032  hlrelat2  35127  elpadd0  35533  bj-ifim123g  37706  bj-ifim2  37713  bj-iforcor  37724  rp-fakeoranass  37738
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
  Copyright terms: Public domain W3C validator