Theorem orcomd 741

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

This proof depends on syntax axioms:   → wi 4   ∨ wo 720

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used by:  olcd  746  stdcndcOLD  858  pm5.54dc  930  r19.30dc  2698  exmid1dc  4339  swopo  4453  sotritrieq  4472  ontriexmidim  4671  ontri2orexmidim  4721  reg3exmidlemwe  4728  acexmidlemcase  6083  2oconcl  6716  nntri3or  6770  nntri2  6771  nntri1  6773  nnsseleq  6778  diffisn  7202  fival  7310  djulclb  7402  exmidomniim  7488  exmidomni  7489  omniwomnimkv  7514  nninfwlpoimlemginf  7523  exmidontriimlem1  7584  3nsssucpw1  7602  addnqprlemfu  7934  mulnqprlemfu  7950  addcanprlemu  7989  cauappcvgprlemladdru  8030  apreap  8924  mulap0r  8952  mul0eqap  9009  nnm1nn0  9616  elnn0z  9669  zleloe  9703  nneoor  9760  nneo  9761  zeo2  9764  uzm1  9970  nn01to3  10034  uzsplit  10517  fzospliti  10603  fzouzsplit  10606  qavgle  10711  xrmaxiflemlub  12040  fz1f1o  12167  fprodsplitdc  12389  fprodcl2lem  12398  ef0lem  12453  zeo3  12661  bezoutlemmain  12801  nninfctlemfo  12843  prmdc  12934  unennn  13347  exmidunben  13376  fnpr2ob  13721  ivthdichlem  15889  plycoeid3  15995  lgsval  16340  lgsfvalg  16341  lgsdilem  16363  wexmiddiffilem  17260  wexmiddifxylem  17262  idjudju  17264  nninfalllem1  17269  nninfall  17270  nninfsellemqall  17276  nninfnfiinf  17284  exmidsbthrlem  17285  sbthomlem  17288  trilpolemeq1  17308