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  4198  swopo  4304  sotritrieq  4323  ontriexmidim  4519  ontri2orexmidim  4569  reg3exmidlemwe  4576  acexmidlemcase  5865  2oconcl  6435  nntri3or  6489  nntri2  6490  nntri1  6492  nnsseleq  6497  diffisn  6888  fival  6964  djulclb  7049  exmidomniim  7134  exmidomni  7135  omniwomnimkv  7160  nninfwlpoimlemginf  7169  exmidontriimlem1  7215  3nsssucpw1  7230  addnqprlemfu  7554  mulnqprlemfu  7570  addcanprlemu  7609  cauappcvgprlemladdru  7650  apreap  8538  mulap0r  8566  mul0eqap  8621  nnm1nn0  9211  elnn0z  9260  zleloe  9294  nneoor  9349  nneo  9350  zeo2  9353  uzm1  9552  nn01to3  9611  uzsplit  10085  fzospliti  10169  fzouzsplit  10172  qavgle  10252  xrmaxiflemlub  11247  fz1f1o  11374  fprodsplitdc  11595  fprodcl2lem  11604  ef0lem  11659  zeo3  11863  bezoutlemmain  11989  prmdc  12120  unennn  12388  exmidunben  12417  lgsval  14187  lgsfvalg  14188  lgsdilem  14210  nninfalllem1  14528  nninfall  14529  nninfsellemqall  14535  exmidsbthrlem  14541  sbthomlem  14544  trilpolemeq1  14559