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  2637  exmid1dc  4215  swopo  4321  sotritrieq  4340  ontriexmidim  4536  ontri2orexmidim  4586  reg3exmidlemwe  4593  acexmidlemcase  5887  2oconcl  6459  nntri3or  6513  nntri2  6514  nntri1  6516  nnsseleq  6521  diffisn  6912  fival  6989  djulclb  7074  exmidomniim  7159  exmidomni  7160  omniwomnimkv  7185  nninfwlpoimlemginf  7194  exmidontriimlem1  7240  3nsssucpw1  7255  addnqprlemfu  7579  mulnqprlemfu  7595  addcanprlemu  7634  cauappcvgprlemladdru  7675  apreap  8564  mulap0r  8592  mul0eqap  8647  nnm1nn0  9237  elnn0z  9286  zleloe  9320  nneoor  9375  nneo  9376  zeo2  9379  uzm1  9578  nn01to3  9637  uzsplit  10112  fzospliti  10196  fzouzsplit  10199  qavgle  10279  xrmaxiflemlub  11276  fz1f1o  11403  fprodsplitdc  11624  fprodcl2lem  11633  ef0lem  11688  zeo3  11893  bezoutlemmain  12019  prmdc  12150  unennn  12423  exmidunben  12452  fnpr2ob  12789  lgsval  14809  lgsfvalg  14810  lgsdilem  14832  nninfalllem1  15162  nninfall  15163  nninfsellemqall  15169  exmidsbthrlem  15175  sbthomlem  15178  trilpolemeq1  15193