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

Theorem orcom 389
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 388 . 2  |-  ( (
ph  \/  ps )  ->  ( ps  \/  ph ) )
2 pm1.4 388 . 2  |-  ( ( ps  \/  ph )  ->  ( ph  \/  ps ) )
31, 2impbii 191 1  |-  ( (
ph  \/  ps )  <->  ( ps  \/  ph )
)
Colors of variables: wff setvar class
Syntax hints:    <-> wb 188    \/ wo 370
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 189  df-or 372
This theorem is referenced by:  orcomd  390  orbi1i  523  orass  527  or32  530  or42  532  orbi1d  709  pm5.61  719  oranabs  867  ordir  876  pm5.17  899  pm5.7  945  pm5.75  948  dn1  977  3orrot  991  3orcomb  995  dfifp7  1432  cadan  1512  cadcomb  1516  stoic1aOLD  1656  19.31v  1790  nf4  2043  19.31  2048  r19.30  2935  eueq2  3212  uncom  3578  reuun2  3726  dfif2  3883  rabrsn  4042  tppreqb  4113  ssunsn2  4131  prel12  4152  disjor  4387  zfpair  4637  somin1  5233  ordtri2  5458  on0eqel  5540  fununi  5649  eliman0  5894  swoer  7391  supgtoreq  7986  cantnflem1d  8193  cantnflem1  8194  cflim2  8693  dffin7-2  8828  fpwwe2lem13  9067  suplem2pr  9478  leloe  9720  mulcan2g  10266  fimaxre  10551  arch  10866  elznn0nn  10951  elznn0  10952  nneo  11019  ltxr  11415  xrleloe  11443  xrrebnd  11463  xmullem2  11551  xmulcom  11552  xmulneg1  11555  xmulf  11558  sqeqori  12386  hashtpg  12641  odd2np1lem  14364  lcmcom  14557  dvdsprime  14637  coprm  14657  lvecvscan2  18335  opprdomn  18525  mplcoe1  18689  mplcoe5  18692  madutpos  19667  restntr  20198  alexsubALTlem2  21063  alexsubALTlem3  21064  xrsxmet  21827  dyaddisj  22554  mdegleb  23013  atandm3  23804  wilthlem2  23994  lgsdir2lem4  24254  tgcolg  24599  hlcomb  24648  axcontlem7  25000  nb3graprlem2  25180  eupath2lem2  25706  eupath2lem3  25707  hvmulcan2  26726  elat2  27993  chrelat2i  28018  atoml2i  28036  or3dir  28102  disjnf  28181  disjorf  28189  disjex  28202  disjexc  28203  disjunsn  28204  funcnv5mpt  28272  elicoelioo  28360  xrdifh  28362  tlt3  28426  orngsqr  28567  ballotlemfc0  29325  ballotlemfcc  29326  bnj563  29553  subfacp1lem6  29908  3orel2  30343  socnv  30405  dfon2lem5  30433  btwnconn1lem14  30867  outsideofcom  30895  outsideofeu  30898  lineunray  30914  ecase13d  30969  elicc3  30973  nn0prpw  30979  bj-dfbi5  31150  bj-consensusALT  31157  bj-nf2  31192  bj-nfn  31219  topdifinfeq  31753  onsucuni3  31770  wl-cases2-dnf  31850  itg2addnclem2  31994  itgaddnclem2  32001  orfa  32315  unitresl  32318  notornotel2  32332  tsbi4  32378  leatb  32858  leat2  32860  isat3  32873  hlrelat2  32968  elpadd0  33374  ifporcor  36105  ifpim2  36115  ifpim23g  36139  ifpim123g  36144  rp-fakeoranass  36158  elprn2  37714  stoweidlem26  37886  2reu3  38609  nb3grprlem2  39455  uhgrvd0nedgb  39545
  Copyright terms: Public domain W3C validator