Theorem orcomd 689

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

Syntax hints:   → wi 4   ∨ wo 670

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 671

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  olcd  694  stabtestimpdc  868  pm5.54dc  871  swopo  4166  sotritrieq  4185  reg3exmidlemwe  4431  acexmidlemcase  5701  2oconcl  6266  nntri3or  6319  nntri2  6320  nntri1  6322  nnsseleq  6327  diffisn  6716  djulclb  6855  exmidomniim  6925  exmidomni  6926  addnqprlemfu  7269  mulnqprlemfu  7285  addcanprlemu  7324  cauappcvgprlemladdru  7365  apreap  8215  mulap0r  8243  mul0eqap  8292  nnm1nn0  8870  elnn0z  8919  zleloe  8953  nneoor  9005  nneo  9006  zeo2  9009  uzm1  9206  nn01to3  9259  uzsplit  9713  fzospliti  9794  fzouzsplit  9797  qavgle  9877  xrmaxiflemlub  10856  fz1f1o  10983  ef0lem  11164  zeo3  11360  bezoutlemmain  11479  unennn  11702  exmidunben  11731  nninfalllem1  12787  nninfall  12788  nninfsellemqall  12795  exmidsbthrlem  12801  sbthomlem  12804  trilpolemeq1  12817