Theorem orcomd 734

Description: Commutation of disjuncts in consequent. (Contributed by NM, 2-Dec-2010.)

Hypothesis

Ref	Expression
orcomd.1	⊢ (𝜑 → (𝜓 ∨ 𝜒))

Assertion

Ref	Expression
orcomd	⊢ (𝜑 → (𝜒 ∨ 𝜓))

Proof of Theorem orcomd

Step	Hyp	Ref	Expression
1		orcomd.1	. 2 ⊢ (𝜑 → (𝜓 ∨ 𝜒))
2		orcom 733	. 2 ⊢ ((𝜓 ∨ 𝜒) ↔ (𝜒 ∨ 𝜓))
3	1, 2	sylib 122	1 ⊢ (𝜑 → (𝜒 ∨ 𝜓))

Syntax hints:   → wi 4   ∨ wo 713

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 714

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  olcd  739  stdcndcOLD  851  pm5.54dc  923  r19.30dc  2678  exmid1dc  4288  swopo  4401  sotritrieq  4420  ontriexmidim  4618  ontri2orexmidim  4668  reg3exmidlemwe  4675  acexmidlemcase  6008  2oconcl  6602  nntri3or  6656  nntri2  6657  nntri1  6659  nnsseleq  6664  diffisn  7077  fival  7163  djulclb  7248  exmidomniim  7334  exmidomni  7335  omniwomnimkv  7360  nninfwlpoimlemginf  7369  exmidontriimlem1  7429  3nsssucpw1  7447  addnqprlemfu  7773  mulnqprlemfu  7789  addcanprlemu  7828  cauappcvgprlemladdru  7869  apreap  8760  mulap0r  8788  mul0eqap  8843  nnm1nn0  9436  elnn0z  9485  zleloe  9519  nneoor  9575  nneo  9576  zeo2  9579  uzm1  9780  nn01to3  9844  uzsplit  10320  fzospliti  10406  fzouzsplit  10409  qavgle  10511  xrmaxiflemlub  11802  fz1f1o  11929  fprodsplitdc  12150  fprodcl2lem  12159  ef0lem  12214  zeo3  12422  bezoutlemmain  12562  nninfctlemfo  12604  prmdc  12695  unennn  13011  exmidunben  13040  fnpr2ob  13416  ivthdichlem  15368  plycoeid3  15474  lgsval  15726  lgsfvalg  15727  lgsdilem  15749  nninfalllem1  16560  nninfall  16561  nninfsellemqall  16567  nninfnfiinf  16575  exmidsbthrlem  16576  sbthomlem  16579  trilpolemeq1  16594