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  7880  mulnqprlemfu  7896  addcanprlemu  7935  cauappcvgprlemladdru  7976  apreap  8866  mulap0r  8894  mul0eqap  8949  nnm1nn0  9542  elnn0z  9595  zleloe  9629  nneoor  9686  nneo  9687  zeo2  9690  uzm1  9891  nn01to3  9955  uzsplit  10433  fzospliti  10519  fzouzsplit  10522  qavgle  10625  xrmaxiflemlub  11941  fz1f1o  12068  fprodsplitdc  12290  fprodcl2lem  12299  ef0lem  12354  zeo3  12562  bezoutlemmain  12702  nninfctlemfo  12744  prmdc  12835  unennn  13169  exmidunben  13198  fnpr2ob  13574  ivthdichlem  15565  plycoeid3  15671  lgsval  15926  lgsfvalg  15927  lgsdilem  15949  nninfalllem1  16835  nninfall  16836  nninfsellemqall  16842  nninfnfiinf  16850  exmidsbthrlem  16851  sbthomlem  16854  trilpolemeq1  16873