Theorem orcomd 719

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

Syntax hints:   → wi 4   ∨ wo 698

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  olcd  724  stdcndcOLD  836  pm5.54dc  908  r19.30dc  2613  exmid1dc  4179  swopo  4284  sotritrieq  4303  ontriexmidim  4499  ontri2orexmidim  4549  reg3exmidlemwe  4556  acexmidlemcase  5837  2oconcl  6407  nntri3or  6461  nntri2  6462  nntri1  6464  nnsseleq  6469  diffisn  6859  fival  6935  djulclb  7020  exmidomniim  7105  exmidomni  7106  omniwomnimkv  7131  exmidontriimlem1  7177  3nsssucpw1  7192  addnqprlemfu  7501  mulnqprlemfu  7517  addcanprlemu  7556  cauappcvgprlemladdru  7597  apreap  8485  mulap0r  8513  mul0eqap  8567  nnm1nn0  9155  elnn0z  9204  zleloe  9238  nneoor  9293  nneo  9294  zeo2  9297  uzm1  9496  nn01to3  9555  uzsplit  10027  fzospliti  10111  fzouzsplit  10114  qavgle  10194  xrmaxiflemlub  11189  fz1f1o  11316  fprodsplitdc  11537  fprodcl2lem  11546  ef0lem  11601  zeo3  11805  bezoutlemmain  11931  prmdc  12062  unennn  12330  exmidunben  12359  lgsval  13545  lgsfvalg  13546  lgsdilem  13568  nninfalllem1  13888  nninfall  13889  nninfsellemqall  13895  exmidsbthrlem  13901  sbthomlem  13904  trilpolemeq1  13919