Theorem orcomd 647

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 646	. 2 ⊢ ((ψ ∨ χ) ↔ (χ ∨ ψ))
3	1, 2	sylib 127	1 ⊢ (φ → (χ ∨ ψ))

Syntax hints:   → wi 4   ∨ wo 628

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  olcd  652  stabtestimpdc  823  pm5.54dc  826  swopo  4034  sotritrieq  4053  acexmidlemcase  5450  2oconcl  5961  nntri3or  6011  nntri2  6012  nntri1  6013  addnqprlemfu  6541  addcanprlemu  6589  cauappcvgprlemladdru  6628  apreap  7371  mulap0r  7399  nnm1nn0  7999  elnn0z  8034  zleloe  8068  nneoor  8116  nneo  8117  zeo2  8120  uzm1  8279  nn01to3  8328  uzsplit  8724  fzospliti  8802  fzouzsplit  8805