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

Theorem orcomd 648
 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 647 . 2 ((𝜓𝜒) ↔ (𝜒𝜓))
31, 2sylib 127 1 (𝜑 → (𝜒𝜓))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∨ wo 629 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630 This theorem depends on definitions:  df-bi 110 This theorem is referenced by:  olcd  653  stabtestimpdc  824  pm5.54dc  827  swopo  4043  sotritrieq  4062  reg3exmidlemwe  4303  acexmidlemcase  5507  2oconcl  6022  nntri3or  6072  nntri2  6073  nntri1  6074  nnsseleq  6079  diffisn  6350  addnqprlemfu  6658  mulnqprlemfu  6674  addcanprlemu  6713  cauappcvgprlemladdru  6754  apreap  7578  mulap0r  7606  nnm1nn0  8223  elnn0z  8258  zleloe  8292  nneoor  8340  nneo  8341  zeo2  8344  uzm1  8503  nn01to3  8552  uzsplit  8954  fzospliti  9032  fzouzsplit  9035
 Copyright terms: Public domain W3C validator