Theorem orcomd 736

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

Syntax hints:   → wi 4   ∨ wo 715

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 716

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  olcd  741  stdcndcOLD  853  pm5.54dc  925  r19.30dc  2679  exmid1dc  4292  swopo  4405  sotritrieq  4424  ontriexmidim  4622  ontri2orexmidim  4672  reg3exmidlemwe  4679  acexmidlemcase  6018  2oconcl  6612  nntri3or  6666  nntri2  6667  nntri1  6669  nnsseleq  6674  diffisn  7087  fival  7174  djulclb  7259  exmidomniim  7345  exmidomni  7346  omniwomnimkv  7371  nninfwlpoimlemginf  7380  exmidontriimlem1  7441  3nsssucpw1  7459  addnqprlemfu  7785  mulnqprlemfu  7801  addcanprlemu  7840  cauappcvgprlemladdru  7881  apreap  8772  mulap0r  8800  mul0eqap  8855  nnm1nn0  9448  elnn0z  9497  zleloe  9531  nneoor  9587  nneo  9588  zeo2  9591  uzm1  9792  nn01to3  9856  uzsplit  10332  fzospliti  10418  fzouzsplit  10421  qavgle  10524  xrmaxiflemlub  11831  fz1f1o  11958  fprodsplitdc  12180  fprodcl2lem  12189  ef0lem  12244  zeo3  12452  bezoutlemmain  12592  nninfctlemfo  12634  prmdc  12725  unennn  13041  exmidunben  13070  fnpr2ob  13446  ivthdichlem  15404  plycoeid3  15510  lgsval  15762  lgsfvalg  15763  lgsdilem  15785  nninfalllem1  16673  nninfall  16674  nninfsellemqall  16680  nninfnfiinf  16688  exmidsbthrlem  16689  sbthomlem  16692  trilpolemeq1  16711