Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  orcomd GIF version

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
StepHypRef Expression
1 orcomd.1 . 2 (𝜑 → (𝜓𝜒))
2 orcom 718 . 2 ((𝜓𝜒) ↔ (𝜒𝜓))
31, 2sylib 121 1 (𝜑 → (𝜒𝜓))
 Colors of variables: wff set class 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  832  pm5.54dc  904  exmid1dc  4131  swopo  4236  sotritrieq  4255  reg3exmidlemwe  4501  acexmidlemcase  5777  2oconcl  6344  nntri3or  6397  nntri2  6398  nntri1  6400  nnsseleq  6405  diffisn  6795  fival  6866  djulclb  6948  exmidomniim  7021  exmidomni  7022  omniwomnimkv  7049  addnqprlemfu  7393  mulnqprlemfu  7409  addcanprlemu  7448  cauappcvgprlemladdru  7489  apreap  8374  mulap0r  8402  mul0eqap  8456  nnm1nn0  9043  elnn0z  9092  zleloe  9126  nneoor  9178  nneo  9179  zeo2  9182  uzm1  9381  nn01to3  9437  uzsplit  9904  fzospliti  9985  fzouzsplit  9988  qavgle  10068  xrmaxiflemlub  11050  fz1f1o  11177  ef0lem  11404  zeo3  11602  bezoutlemmain  11723  unennn  11947  exmidunben  11976  nninfalllem1  13379  nninfall  13380  nninfsellemqall  13387  exmidsbthrlem  13393  sbthomlem  13396  trilpolemeq1  13409
 Copyright terms: Public domain W3C validator