Theorem orcomd 736

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 735	. 2 ⊢ ((𝜓 ∨ 𝜒) ↔ (𝜒 ∨ 𝜓))
3	1, 2	sylib 122	1 ⊢ (𝜑 → (𝜒 ∨ 𝜓))

Syntax hints:   → wi 4   ∨ wo 715

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 716

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  olcd  741  stdcndcOLD  853  pm5.54dc  925  r19.30dc  2680  exmid1dc  4290  swopo  4403  sotritrieq  4422  ontriexmidim  4620  ontri2orexmidim  4670  reg3exmidlemwe  4677  acexmidlemcase  6013  2oconcl  6607  nntri3or  6661  nntri2  6662  nntri1  6664  nnsseleq  6669  diffisn  7082  fival  7169  djulclb  7254  exmidomniim  7340  exmidomni  7341  omniwomnimkv  7366  nninfwlpoimlemginf  7375  exmidontriimlem1  7436  3nsssucpw1  7454  addnqprlemfu  7780  mulnqprlemfu  7796  addcanprlemu  7835  cauappcvgprlemladdru  7876  apreap  8767  mulap0r  8795  mul0eqap  8850  nnm1nn0  9443  elnn0z  9492  zleloe  9526  nneoor  9582  nneo  9583  zeo2  9586  uzm1  9787  nn01to3  9851  uzsplit  10327  fzospliti  10413  fzouzsplit  10416  qavgle  10519  xrmaxiflemlub  11810  fz1f1o  11937  fprodsplitdc  12159  fprodcl2lem  12168  ef0lem  12223  zeo3  12431  bezoutlemmain  12571  nninfctlemfo  12613  prmdc  12704  unennn  13020  exmidunben  13049  fnpr2ob  13425  ivthdichlem  15378  plycoeid3  15484  lgsval  15736  lgsfvalg  15737  lgsdilem  15759  nninfalllem1  16631  nninfall  16632  nninfsellemqall  16638  nninfnfiinf  16646  exmidsbthrlem  16647  sbthomlem  16650  trilpolemeq1  16665