Theorem orcomd 731

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

Syntax hints:   → wi 4   ∨ wo 710

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 711

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  olcd  736  stdcndcOLD  848  pm5.54dc  920  r19.30dc  2654  exmid1dc  4248  swopo  4357  sotritrieq  4376  ontriexmidim  4574  ontri2orexmidim  4624  reg3exmidlemwe  4631  acexmidlemcase  5946  2oconcl  6532  nntri3or  6586  nntri2  6587  nntri1  6589  nnsseleq  6594  diffisn  6997  fival  7079  djulclb  7164  exmidomniim  7250  exmidomni  7251  omniwomnimkv  7276  nninfwlpoimlemginf  7285  exmidontriimlem1  7340  3nsssucpw1  7355  addnqprlemfu  7680  mulnqprlemfu  7696  addcanprlemu  7735  cauappcvgprlemladdru  7776  apreap  8667  mulap0r  8695  mul0eqap  8750  nnm1nn0  9343  elnn0z  9392  zleloe  9426  nneoor  9482  nneo  9483  zeo2  9486  uzm1  9686  nn01to3  9745  uzsplit  10221  fzospliti  10307  fzouzsplit  10310  qavgle  10408  xrmaxiflemlub  11603  fz1f1o  11730  fprodsplitdc  11951  fprodcl2lem  11960  ef0lem  12015  zeo3  12223  bezoutlemmain  12363  nninfctlemfo  12405  prmdc  12496  unennn  12812  exmidunben  12841  fnpr2ob  13216  ivthdichlem  15167  plycoeid3  15273  lgsval  15525  lgsfvalg  15526  lgsdilem  15548  nninfalllem1  16019  nninfall  16020  nninfsellemqall  16026  nninfnfiinf  16034  exmidsbthrlem  16035  sbthomlem  16038  trilpolemeq1  16053