Theorem orcomd 718

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

Syntax hints:   → wi 4   ∨ wo 697

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  olcd  723  stdcndcOLD  831  pm5.54dc  903  exmid1dc  4123  swopo  4228  sotritrieq  4247  reg3exmidlemwe  4493  acexmidlemcase  5769  2oconcl  6336  nntri3or  6389  nntri2  6390  nntri1  6392  nnsseleq  6397  diffisn  6787  fival  6858  djulclb  6940  exmidomniim  7013  exmidomni  7014  addnqprlemfu  7368  mulnqprlemfu  7384  addcanprlemu  7423  cauappcvgprlemladdru  7464  apreap  8349  mulap0r  8377  mul0eqap  8431  nnm1nn0  9018  elnn0z  9067  zleloe  9101  nneoor  9153  nneo  9154  zeo2  9157  uzm1  9356  nn01to3  9409  uzsplit  9872  fzospliti  9953  fzouzsplit  9956  qavgle  10036  xrmaxiflemlub  11017  fz1f1o  11144  ef0lem  11366  zeo3  11565  bezoutlemmain  11686  unennn  11910  exmidunben  11939  nninfalllem1  13203  nninfall  13204  nninfsellemqall  13211  exmidsbthrlem  13217  sbthomlem  13220  trilpolemeq1  13233