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

Theorem orcd 651
Description: Deduction introducing a disjunct. (Contributed by NM, 20-Sep-2007.)
Hypothesis
Ref Expression
orcd.1 (φψ)
Assertion
Ref Expression
orcd (φ → (ψ χ))

Proof of Theorem orcd
StepHypRef Expression
1 orcd.1 . 2 (φψ)
2 orc 632 . 2 (ψ → (ψ χ))
31, 2syl 14 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-io 629
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  olcd  652  pm2.47  658  orim12i  675  dcor  842  sspsstrir  3040  undif3ss  3192  acexmidlem1  5451  poxp  5794  nnm00  6038  ssfiexmid  6254  nqprloc  6528  mullocprlem  6551  recexprlemloc  6603  ltxrlt  6882  zmulcl  8073  nn0lt2  8098  zeo  8119  xrltso  8487  expnegap0  8917
  Copyright terms: Public domain W3C validator