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 ⊢ (𝜑 → (𝜒 ∨ 𝜓))

Syntax hints:   → wi 4   ∨ wo 720

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 721

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  olcd  746  stdcndcOLD  858  pm5.54dc  930  r19.30dc  2698  exmid1dc  4335  swopo  4449  sotritrieq  4468  ontriexmidim  4667  ontri2orexmidim  4717  reg3exmidlemwe  4724  acexmidlemcase  6074  2oconcl  6706  nntri3or  6760  nntri2  6761  nntri1  6763  nnsseleq  6768  diffisn  7191  fival  7298  djulclb  7389  exmidomniim  7475  exmidomni  7476  omniwomnimkv  7501  nninfwlpoimlemginf  7510  exmidontriimlem1  7571  3nsssucpw1  7589  addnqprlemfu  7921  mulnqprlemfu  7937  addcanprlemu  7976  cauappcvgprlemladdru  8017  apreap  8909  mulap0r  8937  mul0eqap  8994  nnm1nn0  9587  elnn0z  9640  zleloe  9674  nneoor  9731  nneo  9732  zeo2  9735  uzm1  9936  nn01to3  10000  uzsplit  10482  fzospliti  10568  fzouzsplit  10571  qavgle  10676  xrmaxiflemlub  11997  fz1f1o  12124  fprodsplitdc  12346  fprodcl2lem  12355  ef0lem  12410  zeo3  12618  bezoutlemmain  12758  nninfctlemfo  12800  prmdc  12891  unennn  13271  exmidunben  13300  fnpr2ob  13644  ivthdichlem  15735  plycoeid3  15841  lgsval  16106  lgsfvalg  16107  lgsdilem  16129  nninfalllem1  17025  nninfall  17026  nninfsellemqall  17032  nninfnfiinf  17040  exmidsbthrlem  17041  sbthomlem  17044  trilpolemeq1  17063