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

Theorem olcd 652
Description: Deduction introducing a disjunct. (Contributed by NM, 11-Apr-2008.) (Proof shortened by Wolf Lammen, 3-Oct-2013.)
Hypothesis
Ref Expression
orcd.1 (φψ)
Assertion
Ref Expression
olcd (φ → (χ ψ))

Proof of Theorem olcd
StepHypRef Expression
1 orcd.1 . . 3 (φψ)
21orcd 651 . 2 (φ → (ψ χ))
32orcomd 647 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:  pm2.48  659  pm2.49  660  orim12i  675  pm1.5  681  dcan  841  dcor  842  sspsstrir  3040  regexmidlem1  4218  nn0suc  4270  nndceq0  4282  acexmidlem1  5451  nntri3or  6011  nndceq  6015  nndcel  6016  nnm00  6038  ssfiexmid  6254  mullocprlem  6550  recexprlemloc  6602  gt0ap0  7388  recexaplem2  7395  nn1m1nn  7693  nn1gt1  7708  ltpnf  8452  mnflt  8454  xrltso  8467  expinnval  8892  exp0  8893  bj-nn0suc0  9384
  Copyright terms: Public domain W3C validator