Theorem orcomd 737

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

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  4315  swopo  4429  sotritrieq  4448  ontriexmidim  4646  ontri2orexmidim  4696  reg3exmidlemwe  4703  acexmidlemcase  6047  2oconcl  6674  nntri3or  6728  nntri2  6729  nntri1  6731  nnsseleq  6736  diffisn  7152  fival  7259  djulclb  7348  exmidomniim  7434  exmidomni  7435  omniwomnimkv  7460  nninfwlpoimlemginf  7469  exmidontriimlem1  7530  3nsssucpw1  7548  addnqprlemfu  7877  mulnqprlemfu  7893  addcanprlemu  7932  cauappcvgprlemladdru  7973  apreap  8863  mulap0r  8891  mul0eqap  8946  nnm1nn0  9539  elnn0z  9592  zleloe  9626  nneoor  9683  nneo  9684  zeo2  9687  uzm1  9888  nn01to3  9952  uzsplit  10430  fzospliti  10516  fzouzsplit  10519  qavgle  10622  xrmaxiflemlub  11937  fz1f1o  12064  fprodsplitdc  12286  fprodcl2lem  12295  ef0lem  12350  zeo3  12558  bezoutlemmain  12698  nninfctlemfo  12740  prmdc  12831  unennn  13165  exmidunben  13194  fnpr2ob  13570  ivthdichlem  15533  plycoeid3  15639  lgsval  15894  lgsfvalg  15895  lgsdilem  15917  nninfalllem1  16803  nninfall  16804  nninfsellemqall  16810  nninfnfiinf  16818  exmidsbthrlem  16819  sbthomlem  16822  trilpolemeq1  16841