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  2690  exmid1dc  4312  swopo  4426  sotritrieq  4445  ontriexmidim  4643  ontri2orexmidim  4693  reg3exmidlemwe  4700  acexmidlemcase  6044  2oconcl  6671  nntri3or  6725  nntri2  6726  nntri1  6728  nnsseleq  6733  diffisn  7149  fival  7256  djulclb  7345  exmidomniim  7431  exmidomni  7432  omniwomnimkv  7457  nninfwlpoimlemginf  7466  exmidontriimlem1  7527  3nsssucpw1  7545  addnqprlemfu  7871  mulnqprlemfu  7887  addcanprlemu  7926  cauappcvgprlemladdru  7967  apreap  8857  mulap0r  8885  mul0eqap  8940  nnm1nn0  9533  elnn0z  9586  zleloe  9620  nneoor  9676  nneo  9677  zeo2  9680  uzm1  9881  nn01to3  9945  uzsplit  10422  fzospliti  10508  fzouzsplit  10511  qavgle  10614  xrmaxiflemlub  11926  fz1f1o  12053  fprodsplitdc  12275  fprodcl2lem  12284  ef0lem  12339  zeo3  12547  bezoutlemmain  12687  nninfctlemfo  12729  prmdc  12820  unennn  13137  exmidunben  13166  fnpr2ob  13542  ivthdichlem  15503  plycoeid3  15609  lgsval  15864  lgsfvalg  15865  lgsdilem  15887  nninfalllem1  16773  nninfall  16774  nninfsellemqall  16780  nninfnfiinf  16788  exmidsbthrlem  16789  sbthomlem  16792  trilpolemeq1  16811