Theorem orcomd 741

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

This proof depends on syntax axioms:   → wi 4   ∨ wo 720

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used by:  olcd  746  stdcndcOLD  858  pm5.54dc  930  r19.30dc  2698  exmid1dc  4337  swopo  4451  sotritrieq  4470  ontriexmidim  4669  ontri2orexmidim  4719  reg3exmidlemwe  4726  acexmidlemcase  6080  2oconcl  6712  nntri3or  6766  nntri2  6767  nntri1  6769  nnsseleq  6774  diffisn  7197  fival  7304  djulclb  7395  exmidomniim  7481  exmidomni  7482  omniwomnimkv  7507  nninfwlpoimlemginf  7516  exmidontriimlem1  7577  3nsssucpw1  7595  addnqprlemfu  7927  mulnqprlemfu  7943  addcanprlemu  7982  cauappcvgprlemladdru  8023  apreap  8916  mulap0r  8944  mul0eqap  9001  nnm1nn0  9606  elnn0z  9659  zleloe  9693  nneoor  9750  nneo  9751  zeo2  9754  uzm1  9955  nn01to3  10019  uzsplit  10501  fzospliti  10587  fzouzsplit  10590  qavgle  10695  xrmaxiflemlub  12016  fz1f1o  12143  fprodsplitdc  12365  fprodcl2lem  12374  ef0lem  12429  zeo3  12637  bezoutlemmain  12777  nninfctlemfo  12819  prmdc  12910  unennn  13290  exmidunben  13319  fnpr2ob  13663  ivthdichlem  15754  plycoeid3  15860  lgsval  16135  lgsfvalg  16136  lgsdilem  16158  wexmiddiffilem  17055  wexmiddifxylem  17057  nninfalllem1  17063  nninfall  17064  nninfsellemqall  17070  nninfnfiinf  17078  exmidsbthrlem  17079  sbthomlem  17082  trilpolemeq1  17101