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

Theorem orcomd 701
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 700 . 2  |-  ( ( ps  \/  ch )  <->  ( ch  \/  ps )
)
31, 2sylib 121 1  |-  ( ph  ->  ( ch  \/  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 680
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 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:  olcd  706  stdcndcOLD  814  pm5.54dc  884  exmid1dc  4081  swopo  4186  sotritrieq  4205  reg3exmidlemwe  4451  acexmidlemcase  5721  2oconcl  6288  nntri3or  6341  nntri2  6342  nntri1  6344  nnsseleq  6349  diffisn  6738  fival  6808  djulclb  6890  exmidomniim  6961  exmidomni  6962  addnqprlemfu  7310  mulnqprlemfu  7326  addcanprlemu  7365  cauappcvgprlemladdru  7406  apreap  8261  mulap0r  8289  mul0eqap  8338  nnm1nn0  8916  elnn0z  8965  zleloe  8999  nneoor  9051  nneo  9052  zeo2  9055  uzm1  9252  nn01to3  9305  uzsplit  9759  fzospliti  9840  fzouzsplit  9843  qavgle  9923  xrmaxiflemlub  10903  fz1f1o  11030  ef0lem  11211  zeo3  11407  bezoutlemmain  11526  unennn  11749  exmidunben  11778  nninfalllem1  12884  nninfall  12885  nninfsellemqall  12892  exmidsbthrlem  12898  sbthomlem  12901  trilpolemeq1  12914
  Copyright terms: Public domain W3C validator