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

Theorem orcom 700
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 699 . 2  |-  ( (
ph  \/  ps )  ->  ( ps  \/  ph ) )
2 pm1.4 699 . 2  |-  ( ( ps  \/  ph )  ->  ( ph  \/  ps ) )
31, 2impbii 125 1  |-  ( (
ph  \/  ps )  <->  ( ps  \/  ph )
)
Colors of variables: wff set class
Syntax hints:    <-> wb 104    \/ wo 680
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 681
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  orcomd  701  orbi1i  735  orass  739  or32  742  or42  744  orbi1d  763  pm5.61  766  oranabs  787  ordir  789  pm2.1dc  805  notnotrdc  811  dcnnOLD  817  pm5.17dc  872  pm5.7dc  921  dn1dc  927  pm5.75  929  3orrot  951  3orcomb  954  excxor  1339  xorcom  1349  19.33b2  1591  nf4dc  1631  nf4r  1632  19.31r  1642  dveeq2  1769  sbequilem  1792  dvelimALT  1961  dvelimfv  1962  dvelimor  1969  eueq2dc  2828  uncom  3188  reuun2  3327  prel12  3666  exmid01  4089  exmidsssnc  4094  ordtriexmid  4405  ordtri2orexmid  4406  ontr2exmid  4408  onsucsssucexmid  4410  ordsoexmid  4445  ordtri2or2exmid  4454  cnvsom  5050  fununi  5159  frec0g  6260  frecabcl  6262  frecsuclem  6269  swoer  6423  inffiexmid  6766  enq0tr  7206  letr  7811  reapmul1  8320  reapneg  8322  reapcotr  8323  remulext1  8324  apsym  8331  mulext1  8337  elznn0nn  9019  elznn0  9020  zapne  9076  nneoor  9104  nn01to3  9358  ltxr  9502  xrletr  9531  maxclpr  10934  minclpr  10948  odd2np1lem  11465  lcmcom  11641  dvdsprime  11699  coprm  11718  bdbl  12567  subctctexmid  12998
  Copyright terms: Public domain W3C validator