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

Step	Hyp	Ref	Expression
1		orcomd.1	. 2 |- ( ph -> ( ps \/ ch ) )
2		orcom 700	. 2 |- ( ( ps \/ ch ) <-> ( ch \/ ps ) )
3	1, 2	sylib 121	1 |- ( ph -> ( ch \/ ps ) )

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