ILE Home 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  860  pm5.54dc  863  swopo  4107  sotritrieq  4126  reg3exmidlemwe  4367  acexmidlemcase  5608  2oconcl  6157  nntri3or  6208  nntri2  6209  nntri1  6211  nnsseleq  6216  diffisn  6561  djulclb  6691  exmidomniim  6741  exmidomni  6742  addnqprlemfu  7063  mulnqprlemfu  7079  addcanprlemu  7118  cauappcvgprlemladdru  7159  apreap  8005  mulap0r  8033  nnm1nn0  8647  elnn0z  8696  zleloe  8730  nneoor  8781  nneo  8782  zeo2  8785  uzm1  8981  nn01to3  9034  uzsplit  9436  fzospliti  9515  fzouzsplit  9518  qavgle  9598  fz1f1o  10654  zeo3  10743  bezoutlemmain  10862  unennn  11085  nninfalllem1  11337  nninfall  11338  nninfsellemqall  11345  exmidsbthrlem  11350
  Copyright terms: Public domain W3C validator