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

Theorem olcd 688
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 687 . 2 (𝜑 → (𝜓𝜒))
32orcomd 683 1 (𝜑 → (𝜒𝜓))
Colors of variables: wff set class
Syntax hints:  wi 4  wo 664
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  pm2.48  695  pm2.49  696  orim12i  711  pm1.5  717  dcan  880  dcor  881  dcun  3388  regexmidlem1  4339  reg2exmidlema  4340  nn0suc  4409  nndceq0  4421  acexmidlem1  5630  nntri3or  6236  nntri2or2  6241  nndceq  6242  nndcel  6243  nnm00  6268  ssfilem  6571  diffitest  6583  tridc  6595  finexdc  6598  fientri3  6605  unsnfidcex  6610  unsnfidcel  6611  fidcenumlemrks  6641  fidcenumlemrk  6642  finomni  6775  exmidfodomrlemeldju  6804  exmidfodomrlemreseldju  6805  exmidfodomrlemr  6807  exmidfodomrlemrALT  6808  mullocprlem  7108  recexprlemloc  7169  gt0ap0  8078  ltap  8084  recexaplem2  8095  nn1m1nn  8412  nn1gt1  8427  ltpnf  9220  mnflt  9222  xrltso  9235  exfzdc  9616  apbtwnz  9646  expnnval  9923  exp0  9924  bc0k  10129  bcpasc  10139  sumdc  10711  zisum  10738  fisum  10742  fisumss  10748  isumss2  10749  fsumsplit  10764  infssuzex  11038  djurclALT  11359  bj-nn0suc0  11502
  Copyright terms: Public domain W3C validator