Theorem orcomd 737

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

Syntax hints:   -> wi 4   \/ wo 716

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  olcd  742  stdcndcOLD  854  pm5.54dc  926  r19.30dc  2690  exmid1dc  4313  swopo  4427  sotritrieq  4446  ontriexmidim  4644  ontri2orexmidim  4694  reg3exmidlemwe  4701  acexmidlemcase  6045  2oconcl  6672  nntri3or  6726  nntri2  6727  nntri1  6729  nnsseleq  6734  diffisn  7150  fival  7257  djulclb  7346  exmidomniim  7432  exmidomni  7433  omniwomnimkv  7458  nninfwlpoimlemginf  7467  exmidontriimlem1  7528  3nsssucpw1  7546  addnqprlemfu  7875  mulnqprlemfu  7891  addcanprlemu  7930  cauappcvgprlemladdru  7971  apreap  8861  mulap0r  8889  mul0eqap  8944  nnm1nn0  9537  elnn0z  9590  zleloe  9624  nneoor  9680  nneo  9681  zeo2  9684  uzm1  9885  nn01to3  9949  uzsplit  10426  fzospliti  10512  fzouzsplit  10515  qavgle  10618  xrmaxiflemlub  11933  fz1f1o  12060  fprodsplitdc  12282  fprodcl2lem  12291  ef0lem  12346  zeo3  12554  bezoutlemmain  12694  nninfctlemfo  12736  prmdc  12827  unennn  13148  exmidunben  13177  fnpr2ob  13553  ivthdichlem  15516  plycoeid3  15622  lgsval  15877  lgsfvalg  15878  lgsdilem  15900  nninfalllem1  16786  nninfall  16787  nninfsellemqall  16793  nninfnfiinf  16801  exmidsbthrlem  16802  sbthomlem  16805  trilpolemeq1  16824