Theorem orcomd 729

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

Syntax hints:   → wi 4   ∨ wo 708

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 709

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  olcd  734  stdcndcOLD  846  pm5.54dc  918  r19.30dc  2624  exmid1dc  4201  swopo  4307  sotritrieq  4326  ontriexmidim  4522  ontri2orexmidim  4572  reg3exmidlemwe  4579  acexmidlemcase  5870  2oconcl  6440  nntri3or  6494  nntri2  6495  nntri1  6497  nnsseleq  6502  diffisn  6893  fival  6969  djulclb  7054  exmidomniim  7139  exmidomni  7140  omniwomnimkv  7165  nninfwlpoimlemginf  7174  exmidontriimlem1  7220  3nsssucpw1  7235  addnqprlemfu  7559  mulnqprlemfu  7575  addcanprlemu  7614  cauappcvgprlemladdru  7655  apreap  8544  mulap0r  8572  mul0eqap  8627  nnm1nn0  9217  elnn0z  9266  zleloe  9300  nneoor  9355  nneo  9356  zeo2  9359  uzm1  9558  nn01to3  9617  uzsplit  10092  fzospliti  10176  fzouzsplit  10179  qavgle  10259  xrmaxiflemlub  11256  fz1f1o  11383  fprodsplitdc  11604  fprodcl2lem  11613  ef0lem  11668  zeo3  11873  bezoutlemmain  11999  prmdc  12130  unennn  12398  exmidunben  12427  fnpr2ob  12759  lgsval  14408  lgsfvalg  14409  lgsdilem  14431  nninfalllem1  14760  nninfall  14761  nninfsellemqall  14767  exmidsbthrlem  14773  sbthomlem  14776  trilpolemeq1  14791