Theorem orcomd 680

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

Syntax hints:   → wi 4   ∨ wo 661

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  olcd  685  stabtestimpdc  857  pm5.54dc  860  swopo  4061  sotritrieq  4080  reg3exmidlemwe  4321  acexmidlemcase  5527  2oconcl  6045  nntri3or  6095  nntri2  6096  nntri1  6097  nnsseleq  6102  diffisn  6377  addnqprlemfu  6750  mulnqprlemfu  6766  addcanprlemu  6805  cauappcvgprlemladdru  6846  apreap  7687  mulap0r  7715  nnm1nn0  8329  elnn0z  8364  zleloe  8398  nneoor  8449  nneo  8450  zeo2  8453  uzm1  8649  nn01to3  8702  uzsplit  9109  fzospliti  9185  fzouzsplit  9188  qavgle  9267  zeo3  10267  bezoutlemmain  10387