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

Theorem olcd 706
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 705 . 2  |-  ( ph  ->  ( ps  \/  ch ) )
32orcomd 701 1  |-  ( ph  ->  ( ch  \/  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 680
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  pm2.48  713  pm2.49  714  orim12i  731  pm1.5  737  dcan  901  dcor  902  dcun  3441  exmidn0m  4092  regexmidlem1  4416  reg2exmidlema  4417  nn0suc  4486  nndceq0  4499  acexmidlem1  5736  nntri3or  6355  nntri2or2  6360  nndceq  6361  nndcel  6362  nnm00  6391  ssfilem  6735  diffitest  6747  tridc  6759  finexdc  6762  fientri3  6769  unsnfidcex  6774  unsnfidcel  6775  fidcenumlemrks  6807  fidcenumlemrk  6808  finomni  6978  exmidfodomrlemeldju  7019  exmidfodomrlemreseldju  7020  exmidfodomrlemr  7022  exmidfodomrlemrALT  7023  exmidaclem  7028  mullocprlem  7342  recexprlemloc  7403  gt0ap0  8351  ltap  8358  recexaplem2  8376  nn1m1nn  8698  nn1gt1  8714  ltpnf  9518  mnflt  9520  xrltso  9533  xrpnfdc  9576  xrmnfdc  9577  exfzdc  9968  apbtwnz  9998  expnnval  10247  exp0  10248  bc0k  10453  bcpasc  10463  xrmaxadd  10981  sumdc  11078  zsumdc  11104  fsum3  11107  fisumss  11112  isumss2  11113  fsumsplit  11127  infssuzex  11549  ctiunctlemudc  11856  suplociccreex  12677  djurclALT  12843  bj-nn0suc0  12982  trilpolemres  13069
  Copyright terms: Public domain W3C validator