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

Theorem orcomd 647
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 646 . 2 ((ψ χ) ↔ (χ ψ))
31, 2sylib 127 1 (φ → (χ ψ))
Colors of variables: wff set class
Syntax hints:  wi 4   wo 628
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 629
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  olcd  652  stabtestimpdc  823  pm5.54dc  826  swopo  4034  sotritrieq  4053  acexmidlemcase  5450  2oconcl  5961  nntri3or  6011  nntri2  6012  nntri1  6013  addnqprlemfu  6541  addcanprlemu  6589  cauappcvgprlemladdru  6628  apreap  7371  mulap0r  7399  nnm1nn0  7999  elnn0z  8034  zleloe  8068  nneoor  8116  nneo  8117  zeo2  8120  uzm1  8279  nn01to3  8328  uzsplit  8724  fzospliti  8802  fzouzsplit  8805
  Copyright terms: Public domain W3C validator