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

Theorem olcd 686
Description: Deduction introducing a disjunct. (Contributed by NM, 11-Apr-2008.) (Proof shortened by Wolf Lammen, 3-Oct-2013.)
Hypothesis
Ref Expression
orcd.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
olcd  |-  ( ph  ->  ( ch  \/  ps ) )

Proof of Theorem olcd
StepHypRef Expression
1 orcd.1 . . 3  |-  ( ph  ->  ps )
21orcd 685 . 2  |-  ( ph  ->  ( ps  \/  ch ) )
32orcomd 681 1  |-  ( ph  ->  ( ch  \/  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 662
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 663
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  pm2.48  693  pm2.49  694  orim12i  709  pm1.5  715  dcan  876  dcor  877  regexmidlem1  4284  reg2exmidlema  4285  nn0suc  4353  nndceq0  4365  acexmidlem1  5539  nntri3or  6137  nntri2or2  6142  nndceq  6143  nndcel  6144  nnm00  6168  ssfilem  6410  diffitest  6421  fientri3  6435  unsnfidcex  6440  unsnfidcel  6441  mullocprlem  6822  recexprlemloc  6883  gt0ap0  7792  ltap  7798  recexaplem2  7809  nn1m1nn  8124  nn1gt1  8139  ltpnf  8932  mnflt  8934  xrltso  8947  exfzdc  9326  apbtwnz  9356  expinnval  9576  exp0  9577  bc0k  9780  bcpasc  9790  sumdc  10333  infssuzex  10489  bj-nn0suc0  10903
  Copyright terms: Public domain W3C validator