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  2692  exmid1dc  4318  swopo  4432  sotritrieq  4451  ontriexmidim  4649  ontri2orexmidim  4699  reg3exmidlemwe  4706  acexmidlemcase  6053  2oconcl  6685  nntri3or  6739  nntri2  6740  nntri1  6742  nnsseleq  6747  diffisn  7163  fival  7270  djulclb  7359  exmidomniim  7445  exmidomni  7446  omniwomnimkv  7471  nninfwlpoimlemginf  7480  exmidontriimlem1  7541  3nsssucpw1  7559  addnqprlemfu  7891  mulnqprlemfu  7907  addcanprlemu  7946  cauappcvgprlemladdru  7987  apreap  8878  mulap0r  8906  mul0eqap  8961  nnm1nn0  9554  elnn0z  9607  zleloe  9641  nneoor  9698  nneo  9699  zeo2  9702  uzm1  9903  nn01to3  9967  uzsplit  10448  fzospliti  10534  fzouzsplit  10537  qavgle  10642  xrmaxiflemlub  11958  fz1f1o  12085  fprodsplitdc  12307  fprodcl2lem  12316  ef0lem  12371  zeo3  12579  bezoutlemmain  12719  nninfctlemfo  12761  prmdc  12852  unennn  13232  exmidunben  13261  fnpr2ob  13604  ivthdichlem  15642  plycoeid3  15748  lgsval  16003  lgsfvalg  16004  lgsdilem  16026  nninfalllem1  16912  nninfall  16913  nninfsellemqall  16919  nninfnfiinf  16927  exmidsbthrlem  16928  sbthomlem  16931  trilpolemeq1  16950