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

Theorem orcomd 689
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 688 . 2 ((𝜓𝜒) ↔ (𝜒𝜓))
31, 2sylib 121 1 (𝜑 → (𝜒𝜓))
Colors of variables: wff set class
Syntax hints:  wi 4  wo 670
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 671
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  olcd  694  stabtestimpdc  868  pm5.54dc  871  swopo  4166  sotritrieq  4185  reg3exmidlemwe  4431  acexmidlemcase  5701  2oconcl  6266  nntri3or  6319  nntri2  6320  nntri1  6322  nnsseleq  6327  diffisn  6716  djulclb  6855  exmidomniim  6925  exmidomni  6926  addnqprlemfu  7269  mulnqprlemfu  7285  addcanprlemu  7324  cauappcvgprlemladdru  7365  apreap  8215  mulap0r  8243  mul0eqap  8292  nnm1nn0  8870  elnn0z  8919  zleloe  8953  nneoor  9005  nneo  9006  zeo2  9009  uzm1  9206  nn01to3  9259  uzsplit  9713  fzospliti  9794  fzouzsplit  9797  qavgle  9877  xrmaxiflemlub  10856  fz1f1o  10983  ef0lem  11164  zeo3  11360  bezoutlemmain  11479  unennn  11702  exmidunben  11731  nninfalllem1  12787  nninfall  12788  nninfsellemqall  12795  exmidsbthrlem  12801  sbthomlem  12804  trilpolemeq1  12817
  Copyright terms: Public domain W3C validator