Theorem orcomd 730

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

Syntax hints:   → wi 4   ∨ wo 709

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 710

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  olcd  735  stdcndcOLD  847  pm5.54dc  919  r19.30dc  2641  exmid1dc  4230  swopo  4338  sotritrieq  4357  ontriexmidim  4555  ontri2orexmidim  4605  reg3exmidlemwe  4612  acexmidlemcase  5914  2oconcl  6494  nntri3or  6548  nntri2  6549  nntri1  6551  nnsseleq  6556  diffisn  6951  fival  7031  djulclb  7116  exmidomniim  7202  exmidomni  7203  omniwomnimkv  7228  nninfwlpoimlemginf  7237  exmidontriimlem1  7283  3nsssucpw1  7298  addnqprlemfu  7622  mulnqprlemfu  7638  addcanprlemu  7677  cauappcvgprlemladdru  7718  apreap  8608  mulap0r  8636  mul0eqap  8691  nnm1nn0  9284  elnn0z  9333  zleloe  9367  nneoor  9422  nneo  9423  zeo2  9426  uzm1  9626  nn01to3  9685  uzsplit  10161  fzospliti  10246  fzouzsplit  10249  qavgle  10330  xrmaxiflemlub  11394  fz1f1o  11521  fprodsplitdc  11742  fprodcl2lem  11751  ef0lem  11806  zeo3  12012  bezoutlemmain  12138  nninfctlemfo  12180  prmdc  12271  unennn  12557  exmidunben  12586  fnpr2ob  12926  ivthdichlem  14830  lgsval  15161  lgsfvalg  15162  lgsdilem  15184  nninfalllem1  15568  nninfall  15569  nninfsellemqall  15575  exmidsbthrlem  15582  sbthomlem  15585  trilpolemeq1  15600