Theorem orcomd 729

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

Syntax hints:   → wi 4   ∨ wo 708

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 709

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  olcd  734  stdcndcOLD  846  pm5.54dc  918  r19.30dc  2624  exmid1dc  4200  swopo  4306  sotritrieq  4325  ontriexmidim  4521  ontri2orexmidim  4571  reg3exmidlemwe  4578  acexmidlemcase  5869  2oconcl  6439  nntri3or  6493  nntri2  6494  nntri1  6496  nnsseleq  6501  diffisn  6892  fival  6968  djulclb  7053  exmidomniim  7138  exmidomni  7139  omniwomnimkv  7164  nninfwlpoimlemginf  7173  exmidontriimlem1  7219  3nsssucpw1  7234  addnqprlemfu  7558  mulnqprlemfu  7574  addcanprlemu  7613  cauappcvgprlemladdru  7654  apreap  8543  mulap0r  8571  mul0eqap  8626  nnm1nn0  9216  elnn0z  9265  zleloe  9299  nneoor  9354  nneo  9355  zeo2  9358  uzm1  9557  nn01to3  9616  uzsplit  10091  fzospliti  10175  fzouzsplit  10178  qavgle  10258  xrmaxiflemlub  11255  fz1f1o  11382  fprodsplitdc  11603  fprodcl2lem  11612  ef0lem  11667  zeo3  11872  bezoutlemmain  11998  prmdc  12129  unennn  12397  exmidunben  12426  fnpr2ob  12758  lgsval  14375  lgsfvalg  14376  lgsdilem  14398  nninfalllem1  14727  nninfall  14728  nninfsellemqall  14734  exmidsbthrlem  14740  sbthomlem  14743  trilpolemeq1  14758