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

Theorem orcomd 681
 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 680 . 2 ((𝜓𝜒) ↔ (𝜒𝜓))
31, 2sylib 120 1 (𝜑 → (𝜒𝜓))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∨ wo 662 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663 This theorem depends on definitions:  df-bi 115 This theorem is referenced by:  olcd  686  stabtestimpdc  858  pm5.54dc  861  swopo  4089  sotritrieq  4108  reg3exmidlemwe  4349  acexmidlemcase  5558  2oconcl  6106  nntri3or  6157  nntri2  6158  nntri1  6160  nnsseleq  6165  diffisn  6449  addnqprlemfu  6864  mulnqprlemfu  6880  addcanprlemu  6919  cauappcvgprlemladdru  6960  apreap  7806  mulap0r  7834  nnm1nn0  8448  elnn0z  8497  zleloe  8531  nneoor  8582  nneo  8583  zeo2  8586  uzm1  8782  nn01to3  8835  uzsplit  9237  fzospliti  9314  fzouzsplit  9317  qavgle  9397  fz1f1o  10399  zeo3  10475  bezoutlemmain  10594  unennn  10817
 Copyright terms: Public domain W3C validator