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

Theorem orcom 657
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 656 . 2  |-  ( (
ph  \/  ps )  ->  ( ps  \/  ph ) )
2 pm1.4 656 . 2  |-  ( ( ps  \/  ph )  ->  ( ph  \/  ps ) )
31, 2impbii 121 1  |-  ( (
ph  \/  ps )  <->  ( ps  \/  ph )
)
Colors of variables: wff set class
Syntax hints:    <-> wb 102    \/ wo 639
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  orcomd  658  orbi1i  690  orass  694  or32  697  or42  699  orbi1d  715  pm5.61  718  oranabs  739  ordir  741  pm2.1dc  756  notnotrdc  762  pm5.17dc  821  testbitestn  834  pm5.7dc  872  dn1dc  878  pm5.75  880  3orrot  902  3orcomb  905  excxor  1285  xorcom  1295  19.33b2  1536  nf4dc  1576  nf4r  1577  19.31r  1587  dveeq2  1712  sbequilem  1735  dvelimALT  1902  dvelimfv  1903  dvelimor  1910  eueq2dc  2737  uncom  3115  reuun2  3248  prel12  3570  ordtriexmid  4275  ordtri2orexmid  4276  ontr2exmid  4278  onsucsssucexmid  4280  ordsoexmid  4314  ordtri2or2exmid  4324  cnvsom  4889  fununi  4995  frec0g  6014  frecsuclem3  6021  swoer  6165  enq0tr  6590  letr  7160  reapmul1  7660  reapneg  7662  reapcotr  7663  remulext1  7664  apsym  7671  mulext1  7677  elznn0nn  8316  elznn0  8317  zapne  8373  nneoor  8399  nn01to3  8649  ltxr  8796  xrletr  8825  odd2np1lem  10183
  Copyright terms: Public domain W3C validator