ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  orcom Unicode version

Theorem orcom 728
Description: Commutative law for disjunction. Theorem *4.31 of [WhiteheadRussell] p. 118. (Contributed by NM, 5-Aug-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 727 . 2  |-  ( (
ph  \/  ps )  ->  ( ps  \/  ph ) )
2 pm1.4 727 . 2  |-  ( ( ps  \/  ph )  ->  ( ph  \/  ps ) )
31, 2impbii 126 1  |-  ( (
ph  \/  ps )  <->  ( ps  \/  ph )
)
Colors of variables: wff set class
Syntax hints:    <-> wb 105    \/ wo 708
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  orcomd  729  orbi1i  763  orass  767  or32  770  or42  772  orbi1d  791  pm5.61  794  oranabs  815  ordir  817  pm2.1dc  837  notnotrdc  843  dcnnOLD  849  pm5.17dc  904  pm5.7dc  954  dn1dc  960  pm5.75  962  3orrot  984  3orcomb  987  excxor  1378  xorcom  1388  19.33b2  1629  nf4dc  1670  nf4r  1671  19.31r  1681  dveeq2  1815  sbequilem  1838  dvelimALT  2010  dvelimfv  2011  dvelimor  2018  eueq2dc  2910  uncom  3279  reuun2  3418  prel12  3771  exmid01  4198  exmidsssnc  4203  ordtriexmid  4520  ordtri2orexmid  4522  ontr2exmid  4524  onsucsssucexmid  4526  ordsoexmid  4561  ordtri2or2exmid  4570  cnvsom  5172  fununi  5284  frec0g  6397  frecabcl  6399  frecsuclem  6406  swoer  6562  inffiexmid  6905  exmidontriimlem1  7219  enq0tr  7432  letr  8038  reapmul1  8550  reapneg  8552  reapcotr  8553  remulext1  8554  apsym  8561  mulext1  8567  elznn0nn  9265  elznn0  9266  zapne  9325  nneoor  9353  nn01to3  9615  ltxr  9773  xrletr  9806  maxclpr  11226  minclpr  11240  odd2np1lem  11871  lcmcom  12058  dvdsprime  12116  coprm  12138  bdbl  13896  cos11  14167  lgsdir2lem4  14325  subctctexmid  14632
  Copyright terms: Public domain W3C validator