Theorem orcomd 737

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

Syntax hints:   → wi 4   ∨ wo 716

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 717

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  olcd  742  stdcndcOLD  854  pm5.54dc  926  r19.30dc  2692  exmid1dc  4318  swopo  4432  sotritrieq  4451  ontriexmidim  4649  ontri2orexmidim  4699  reg3exmidlemwe  4706  acexmidlemcase  6053  2oconcl  6685  nntri3or  6739  nntri2  6740  nntri1  6742  nnsseleq  6747  diffisn  7163  fival  7270  djulclb  7359  exmidomniim  7445  exmidomni  7446  omniwomnimkv  7471  nninfwlpoimlemginf  7480  exmidontriimlem1  7541  3nsssucpw1  7559  addnqprlemfu  7891  mulnqprlemfu  7907  addcanprlemu  7946  cauappcvgprlemladdru  7987  apreap  8879  mulap0r  8907  mul0eqap  8964  nnm1nn0  9557  elnn0z  9610  zleloe  9644  nneoor  9701  nneo  9702  zeo2  9705  uzm1  9906  nn01to3  9970  uzsplit  10451  fzospliti  10537  fzouzsplit  10540  qavgle  10645  xrmaxiflemlub  11961  fz1f1o  12088  fprodsplitdc  12310  fprodcl2lem  12319  ef0lem  12374  zeo3  12582  bezoutlemmain  12722  nninfctlemfo  12764  prmdc  12855  unennn  13235  exmidunben  13264  fnpr2ob  13607  ivthdichlem  15645  plycoeid3  15751  lgsval  16006  lgsfvalg  16007  lgsdilem  16029  nninfalllem1  16925  nninfall  16926  nninfsellemqall  16932  nninfnfiinf  16940  exmidsbthrlem  16941  sbthomlem  16944  trilpolemeq1  16963