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

Theorem olcd 653
 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 652 . 2 (𝜑 → (𝜓𝜒))
32orcomd 648 1 (𝜑 → (𝜒𝜓))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∨ wo 629 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 630 This theorem depends on definitions:  df-bi 110 This theorem is referenced by:  pm2.48  660  pm2.49  661  orim12i  676  pm1.5  682  dcan  842  dcor  843  sspsstrir  3046  regexmidlem1  4258  reg2exmidlema  4259  nn0suc  4327  nndceq0  4339  acexmidlem1  5508  nntri3or  6072  nntri2or2  6076  nndceq  6077  nndcel  6078  nnm00  6102  ssfiexmid  6336  diffitest  6344  fientri3  6353  mullocprlem  6668  recexprlemloc  6729  gt0ap0  7616  ltap  7622  recexaplem2  7633  nn1m1nn  7932  nn1gt1  7947  ltpnf  8702  mnflt  8704  xrltso  8717  expinnval  9258  exp0  9259  bj-nn0suc0  10075
 Copyright terms: Public domain W3C validator