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

Theorem olcd 640
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 639 . 2 (φ → (ψ χ))
32orcomd 635 1 (φ → (χ ψ))
Colors of variables: wff set class
Syntax hints:  wi 4   wo 616
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 617
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  pm2.48  647  pm2.49  648  orim12i  663  pm1.5  669  dcan  828  dcor  829  sspsstrir  3019  regexmidlem1  4198  nn0suc  4250  nndceq0  4262  acexmidlem1  5428  nntri3or  5983  nndceq  5986  nndcel  5987  nnm00  6009  mullocprlem  6408  recexprlemloc  6459  bj-nn0suc0  7311
  Copyright terms: Public domain W3C validator