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  4285  swopo  4398  sotritrieq  4417  ontriexmidim  4615  ontri2orexmidim  4665  reg3exmidlemwe  4672  acexmidlemcase  6005  2oconcl  6598  nntri3or  6652  nntri2  6653  nntri1  6655  nnsseleq  6660  diffisn  7068  fival  7153  djulclb  7238  exmidomniim  7324  exmidomni  7325  omniwomnimkv  7350  nninfwlpoimlemginf  7359  exmidontriimlem1  7419  3nsssucpw1  7437  addnqprlemfu  7763  mulnqprlemfu  7779  addcanprlemu  7818  cauappcvgprlemladdru  7859  apreap  8750  mulap0r  8778  mul0eqap  8833  nnm1nn0  9426  elnn0z  9475  zleloe  9509  nneoor  9565  nneo  9566  zeo2  9569  uzm1  9770  nn01to3  9829  uzsplit  10305  fzospliti  10391  fzouzsplit  10394  qavgle  10495  xrmaxiflemlub  11780  fz1f1o  11907  fprodsplitdc  12128  fprodcl2lem  12137  ef0lem  12192  zeo3  12400  bezoutlemmain  12540  nninfctlemfo  12582  prmdc  12673  unennn  12989  exmidunben  13018  fnpr2ob  13394  ivthdichlem  15346  plycoeid3  15452  lgsval  15704  lgsfvalg  15705  lgsdilem  15727  nninfalllem1  16488  nninfall  16489  nninfsellemqall  16495  nninfnfiinf  16503  exmidsbthrlem  16504  sbthomlem  16507  trilpolemeq1  16522