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  2644  exmid1dc  4234  swopo  4342  sotritrieq  4361  ontriexmidim  4559  ontri2orexmidim  4609  reg3exmidlemwe  4616  acexmidlemcase  5920  2oconcl  6506  nntri3or  6560  nntri2  6561  nntri1  6563  nnsseleq  6568  diffisn  6963  fival  7045  djulclb  7130  exmidomniim  7216  exmidomni  7217  omniwomnimkv  7242  nninfwlpoimlemginf  7251  exmidontriimlem1  7306  3nsssucpw1  7321  addnqprlemfu  7646  mulnqprlemfu  7662  addcanprlemu  7701  cauappcvgprlemladdru  7742  apreap  8633  mulap0r  8661  mul0eqap  8716  nnm1nn0  9309  elnn0z  9358  zleloe  9392  nneoor  9447  nneo  9448  zeo2  9451  uzm1  9651  nn01to3  9710  uzsplit  10186  fzospliti  10271  fzouzsplit  10274  qavgle  10367  xrmaxiflemlub  11432  fz1f1o  11559  fprodsplitdc  11780  fprodcl2lem  11789  ef0lem  11844  zeo3  12052  bezoutlemmain  12192  nninfctlemfo  12234  prmdc  12325  unennn  12641  exmidunben  12670  fnpr2ob  13044  ivthdichlem  14973  plycoeid3  15079  lgsval  15331  lgsfvalg  15332  lgsdilem  15354  nninfalllem1  15741  nninfall  15742  nninfsellemqall  15748  nninfnfiinf  15756  exmidsbthrlem  15757  sbthomlem  15760  trilpolemeq1  15775