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  2634  exmid1dc  4212  swopo  4318  sotritrieq  4337  ontriexmidim  4533  ontri2orexmidim  4583  reg3exmidlemwe  4590  acexmidlemcase  5883  2oconcl  6454  nntri3or  6508  nntri2  6509  nntri1  6511  nnsseleq  6516  diffisn  6907  fival  6983  djulclb  7068  exmidomniim  7153  exmidomni  7154  omniwomnimkv  7179  nninfwlpoimlemginf  7188  exmidontriimlem1  7234  3nsssucpw1  7249  addnqprlemfu  7573  mulnqprlemfu  7589  addcanprlemu  7628  cauappcvgprlemladdru  7669  apreap  8558  mulap0r  8586  mul0eqap  8641  nnm1nn0  9231  elnn0z  9280  zleloe  9314  nneoor  9369  nneo  9370  zeo2  9373  uzm1  9572  nn01to3  9631  uzsplit  10106  fzospliti  10190  fzouzsplit  10193  qavgle  10273  xrmaxiflemlub  11270  fz1f1o  11397  fprodsplitdc  11618  fprodcl2lem  11627  ef0lem  11682  zeo3  11887  bezoutlemmain  12013  prmdc  12144  unennn  12412  exmidunben  12441  fnpr2ob  12778  lgsval  14701  lgsfvalg  14702  lgsdilem  14724  nninfalllem1  15054  nninfall  15055  nninfsellemqall  15061  exmidsbthrlem  15067  sbthomlem  15070  trilpolemeq1  15085