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

Theorem orcomd 681
Description: Commutation of disjuncts in consequent. (Contributed by NM, 2-Dec-2010.)
Hypothesis
Ref Expression
orcomd.1  |-  ( ph  ->  ( ps  \/  ch ) )
Assertion
Ref Expression
orcomd  |-  ( ph  ->  ( ch  \/  ps ) )

Proof of Theorem orcomd
StepHypRef Expression
1 orcomd.1 . 2  |-  ( ph  ->  ( ps  \/  ch ) )
2 orcom 680 . 2  |-  ( ( ps  \/  ch )  <->  ( ch  \/  ps )
)
31, 2sylib 120 1  |-  ( ph  ->  ( ch  \/  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 662
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  olcd  686  stabtestimpdc  858  pm5.54dc  861  swopo  4096  sotritrieq  4115  reg3exmidlemwe  4356  acexmidlemcase  5584  2oconcl  6133  nntri3or  6184  nntri2  6185  nntri1  6187  nnsseleq  6192  diffisn  6537  djulclb  6652  exmidomniim  6700  exmidomni  6701  addnqprlemfu  7020  mulnqprlemfu  7036  addcanprlemu  7075  cauappcvgprlemladdru  7116  apreap  7962  mulap0r  7990  nnm1nn0  8604  elnn0z  8657  zleloe  8691  nneoor  8742  nneo  8743  zeo2  8746  uzm1  8942  nn01to3  8995  uzsplit  9397  fzospliti  9474  fzouzsplit  9477  qavgle  9557  fz1f1o  10570  zeo3  10646  bezoutlemmain  10765  unennn  10988
  Copyright terms: Public domain W3C validator