Theorem orcomd 718

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 717	. 2 |- ( ( ps \/ ch ) <-> ( ch \/ ps ) )
3	1, 2	sylib 121	1 |- ( ph -> ( ch \/ ps ) )

Syntax hints:   -> wi 4   \/ wo 697

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 698

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  olcd  723  stdcndcOLD  831  pm5.54dc  903  exmid1dc  4118  swopo  4223  sotritrieq  4242  reg3exmidlemwe  4488  acexmidlemcase  5762  2oconcl  6329  nntri3or  6382  nntri2  6383  nntri1  6385  nnsseleq  6390  diffisn  6780  fival  6851  djulclb  6933  exmidomniim  7006  exmidomni  7007  addnqprlemfu  7361  mulnqprlemfu  7377  addcanprlemu  7416  cauappcvgprlemladdru  7457  apreap  8342  mulap0r  8370  mul0eqap  8424  nnm1nn0  9011  elnn0z  9060  zleloe  9094  nneoor  9146  nneo  9147  zeo2  9150  uzm1  9349  nn01to3  9402  uzsplit  9865  fzospliti  9946  fzouzsplit  9949  qavgle  10029  xrmaxiflemlub  11010  fz1f1o  11137  ef0lem  11355  zeo3  11554  bezoutlemmain  11675  unennn  11899  exmidunben  11928  nninfalllem1  13192  nninfall  13193  nninfsellemqall  13200  exmidsbthrlem  13206  sbthomlem  13209  trilpolemeq1  13222