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

Theorem orcom 702
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 701 . 2  |-  ( (
ph  \/  ps )  ->  ( ps  \/  ph ) )
2 pm1.4 701 . 2  |-  ( ( ps  \/  ph )  ->  ( ph  \/  ps ) )
31, 2impbii 125 1  |-  ( (
ph  \/  ps )  <->  ( ps  \/  ph )
)
Colors of variables: wff set class
Syntax hints:    <-> wb 104    \/ wo 682
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 683
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  orcomd  703  orbi1i  737  orass  741  or32  744  or42  746  orbi1d  765  pm5.61  768  oranabs  789  ordir  791  pm2.1dc  807  notnotrdc  813  dcnnOLD  819  pm5.17dc  874  pm5.7dc  923  dn1dc  929  pm5.75  931  3orrot  953  3orcomb  956  excxor  1341  xorcom  1351  19.33b2  1593  nf4dc  1633  nf4r  1634  19.31r  1644  dveeq2  1771  sbequilem  1794  dvelimALT  1963  dvelimfv  1964  dvelimor  1971  eueq2dc  2830  uncom  3190  reuun2  3329  prel12  3668  exmid01  4091  exmidsssnc  4096  ordtriexmid  4407  ordtri2orexmid  4408  ontr2exmid  4410  onsucsssucexmid  4412  ordsoexmid  4447  ordtri2or2exmid  4456  cnvsom  5052  fununi  5161  frec0g  6262  frecabcl  6264  frecsuclem  6271  swoer  6425  inffiexmid  6768  enq0tr  7210  letr  7815  reapmul1  8324  reapneg  8326  reapcotr  8327  remulext1  8328  apsym  8335  mulext1  8341  elznn0nn  9026  elznn0  9027  zapne  9083  nneoor  9111  nn01to3  9365  ltxr  9517  xrletr  9546  maxclpr  10949  minclpr  10963  odd2np1lem  11481  lcmcom  11657  dvdsprime  11715  coprm  11734  bdbl  12583  subctctexmid  13092
  Copyright terms: Public domain W3C validator