Theorem orcomd 734

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

Syntax hints:   → wi 4   ∨ wo 713

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 714

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  olcd  739  stdcndcOLD  851  pm5.54dc  923  r19.30dc  2678  exmid1dc  4284  swopo  4397  sotritrieq  4416  ontriexmidim  4614  ontri2orexmidim  4664  reg3exmidlemwe  4671  acexmidlemcase  6002  2oconcl  6593  nntri3or  6647  nntri2  6648  nntri1  6650  nnsseleq  6655  diffisn  7063  fival  7145  djulclb  7230  exmidomniim  7316  exmidomni  7317  omniwomnimkv  7342  nninfwlpoimlemginf  7351  exmidontriimlem1  7411  3nsssucpw1  7429  addnqprlemfu  7755  mulnqprlemfu  7771  addcanprlemu  7810  cauappcvgprlemladdru  7851  apreap  8742  mulap0r  8770  mul0eqap  8825  nnm1nn0  9418  elnn0z  9467  zleloe  9501  nneoor  9557  nneo  9558  zeo2  9561  uzm1  9761  nn01to3  9820  uzsplit  10296  fzospliti  10382  fzouzsplit  10385  qavgle  10486  xrmaxiflemlub  11767  fz1f1o  11894  fprodsplitdc  12115  fprodcl2lem  12124  ef0lem  12179  zeo3  12387  bezoutlemmain  12527  nninfctlemfo  12569  prmdc  12660  unennn  12976  exmidunben  13005  fnpr2ob  13381  ivthdichlem  15333  plycoeid3  15439  lgsval  15691  lgsfvalg  15692  lgsdilem  15714  nninfalllem1  16404  nninfall  16405  nninfsellemqall  16411  nninfnfiinf  16419  exmidsbthrlem  16420  sbthomlem  16423  trilpolemeq1  16438