Theorem orcomd 730

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

Syntax hints:   → wi 4   ∨ wo 709

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 710

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  olcd  735  stdcndcOLD  847  pm5.54dc  919  r19.30dc  2641  exmid1dc  4229  swopo  4337  sotritrieq  4356  ontriexmidim  4554  ontri2orexmidim  4604  reg3exmidlemwe  4611  acexmidlemcase  5913  2oconcl  6492  nntri3or  6546  nntri2  6547  nntri1  6549  nnsseleq  6554  diffisn  6949  fival  7029  djulclb  7114  exmidomniim  7200  exmidomni  7201  omniwomnimkv  7226  nninfwlpoimlemginf  7235  exmidontriimlem1  7281  3nsssucpw1  7296  addnqprlemfu  7620  mulnqprlemfu  7636  addcanprlemu  7675  cauappcvgprlemladdru  7716  apreap  8606  mulap0r  8634  mul0eqap  8689  nnm1nn0  9281  elnn0z  9330  zleloe  9364  nneoor  9419  nneo  9420  zeo2  9423  uzm1  9623  nn01to3  9682  uzsplit  10158  fzospliti  10243  fzouzsplit  10246  qavgle  10327  xrmaxiflemlub  11391  fz1f1o  11518  fprodsplitdc  11739  fprodcl2lem  11748  ef0lem  11803  zeo3  12009  bezoutlemmain  12135  nninfctlemfo  12177  prmdc  12268  unennn  12554  exmidunben  12583  fnpr2ob  12923  ivthdichlem  14805  lgsval  15120  lgsfvalg  15121  lgsdilem  15143  nninfalllem1  15498  nninfall  15499  nninfsellemqall  15505  exmidsbthrlem  15512  sbthomlem  15515  trilpolemeq1  15530