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

Theorem olcd 663
 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 662 . 2 (𝜑 → (𝜓𝜒))
32orcomd 658 1 (𝜑 → (𝜒𝜓))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∨ wo 639 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640 This theorem depends on definitions:  df-bi 114 This theorem is referenced by:  pm2.48  670  pm2.49  671  orim12i  686  pm1.5  692  dcan  853  dcor  854  sspsstrir  3074  regexmidlem1  4286  reg2exmidlema  4287  nn0suc  4355  nndceq0  4367  acexmidlem1  5536  nntri3or  6103  nntri2or2  6107  nndceq  6108  nndcel  6109  nnm00  6133  ssfiexmid  6367  diffitest  6375  fientri3  6384  mullocprlem  6726  recexprlemloc  6787  gt0ap0  7690  ltap  7696  recexaplem2  7707  nn1m1nn  8008  nn1gt1  8023  ltpnf  8803  mnflt  8805  xrltso  8818  expinnval  9423  exp0  9424  bc0k  9624  bcpasc  9634  bj-nn0suc0  10462
 Copyright terms: Public domain W3C validator