Theorem orcomd 741

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

This proof depends on syntax axioms:   -> wi 4   \/ wo 720

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used by:  olcd  746  stdcndcOLD  858  pm5.54dc  930  r19.30dc  2698  exmid1dc  4339  swopo  4453  sotritrieq  4472  ontriexmidim  4671  ontri2orexmidim  4721  reg3exmidlemwe  4728  acexmidlemcase  6083  2oconcl  6717  nntri3or  6771  nntri2  6772  nntri1  6774  nnsseleq  6779  diffisn  7203  fival  7309  djulclb  7401  exmidomniim  7487  exmidomni  7488  omniwomnimkv  7513  nninfwlpoimlemginf  7522  exmidontriimlem1  7583  3nsssucpw1  7601  addnqprlemfu  7933  mulnqprlemfu  7949  addcanprlemu  7988  cauappcvgprlemladdru  8029  apreap  8923  mulap0r  8951  mul0eqap  9008  nnm1nn0  9615  elnn0z  9666  zleloe  9700  nneoor  9758  nneo  9759  zeo2  9762  uzm1  9968  nn01to3  10032  uzsplit  10515  fzospliti  10601  fzouzsplit  10604  qavgle  10709  xrmaxiflemlub  12038  fz1f1o  12165  fprodsplitdc  12387  fprodcl2lem  12396  ef0lem  12451  zeo3  12659  bezoutlemmain  12799  nninfctlemfo  12841  prmdc  12932  unennn  13345  exmidunben  13374  fnpr2ob  13719  ivthdichlem  15894  plycoeid3  16000  lgsval  16345  lgsfvalg  16346  lgsdilem  16368  wexmiddiffilem  17265  wexmiddifxylem  17267  idjudju  17269  nninfalllem1  17274  nninfall  17275  nninfsellemqall  17281  nninfnfiinf  17289  exmidsbthrlem  17290  sbthomlem  17293  trilpolemeq1  17313