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  978  3orcomb  982  cadan  1445  stoic1a  1590  19.31v  1716  nf4  1946  19.31  1952  r19.30  2986  eueq2  3257  uncom  3630  reuun2  3763  dfif2  3924  rabrsn  4081  tppreqb  4152  ssunsn2  4170  prel12  4188  disjor  4417  zfpair  4670  ordtri2  4899  on0eqel  4981  somin1  5389  fununi  5640  eliman0  5881  swoer  7337  supgtoreq  7926  cantnflem1d  8105  cantnflem1  8106  cantnflem1dOLD  8128  cantnflem1OLD  8129  cflim2  8641  dffin7-2  8776  fpwwe2lem13  9018  suplem2pr  9429  leloe  9669  mulcan2g  10204  fimaxre  10491  arch  10793  elznn0nn  10879  elznn0  10880  nneo  10947  ltxr  11328  xrleloe  11354  xrrebnd  11373  xmullem2  11461  xmulcom  11462  xmulneg1  11465  xmulf  11468  sqeqori  12254  hashtpg  12497  odd2np1lem  13917  dvdsprime  14102  coprm  14113  lvecvscan2  17626  opprdomn  17818  mplcoe1  17995  mplcoe5  17999  mplcoe2OLD  18001  madutpos  19011  restntr  19549  alexsubALTlem2  20414  alexsubALTlem3  20415  xrsxmet  21180  dyaddisj  21871  mdegleb  22330  atandm3  23074  wilthlem2  23208  lgsdir2lem4  23466  tgcolg  23806  hlcomb  23852  axcontlem7  24138  nb3graprlem2  24317  eupath2lem2  24843  eupath2lem3  24844  hvmulcan2  25855  elat2  27124  chrelat2i  27149  atoml2i  27167  or3dir  27233  disjnf  27298  disjorf  27305  disjex  27316  disjexc  27317  disjunsn  27318  funcnv5mpt  27376  elicoelioo  27454  xrdifh  27456  tlt3  27519  orngsqr  27660  ballotlemfc0  28297  ballotlemfcc  28298  subfacp1lem6  28495  3orel2  28954  socnv  29162  dfon2lem5  29187  btwnconn1lem14  29718  outsideofcom  29746  outsideofeu  29749  lineunray  29765  itg2addnclem2  30035  itgaddnclem2  30042  ecase13d  30099  elicc3  30103  nn0prpw  30109  orfa  30447  unitresl  30450  notornotel2  30464  tsbi4  30511  lcmcom  31168  elprn2  31544  stoweidlem26  31693  2reu3  32027  bnj563  33507  bj-dfbi5  33850  bj-dfif7  33865  bj-nf2  33910  bj-nfn  33933  leatb  34719  leat2  34721  isat3  34734  hlrelat2  34829  elpadd0  35235  rp-fakeoranass  37403
  Copyright terms: Public domain W3C validator