Theorem orcomd 729

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

Syntax hints:   → wi 4   ∨ wo 708

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 709

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  olcd  734  stdcndcOLD  846  pm5.54dc  918  r19.30dc  2624  exmid1dc  4200  swopo  4306  sotritrieq  4325  ontriexmidim  4521  ontri2orexmidim  4571  reg3exmidlemwe  4578  acexmidlemcase  5869  2oconcl  6439  nntri3or  6493  nntri2  6494  nntri1  6496  nnsseleq  6501  diffisn  6892  fival  6968  djulclb  7053  exmidomniim  7138  exmidomni  7139  omniwomnimkv  7164  nninfwlpoimlemginf  7173  exmidontriimlem1  7219  3nsssucpw1  7234  addnqprlemfu  7558  mulnqprlemfu  7574  addcanprlemu  7613  cauappcvgprlemladdru  7654  apreap  8542  mulap0r  8570  mul0eqap  8625  nnm1nn0  9215  elnn0z  9264  zleloe  9298  nneoor  9353  nneo  9354  zeo2  9357  uzm1  9556  nn01to3  9615  uzsplit  10089  fzospliti  10173  fzouzsplit  10176  qavgle  10256  xrmaxiflemlub  11251  fz1f1o  11378  fprodsplitdc  11599  fprodcl2lem  11608  ef0lem  11663  zeo3  11867  bezoutlemmain  11993  prmdc  12124  unennn  12392  exmidunben  12421  lgsval  14298  lgsfvalg  14299  lgsdilem  14321  nninfalllem1  14639  nninfall  14640  nninfsellemqall  14646  exmidsbthrlem  14652  sbthomlem  14655  trilpolemeq1  14670