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

Theorem olcd 724
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 723 . 2  |-  ( ph  ->  ( ps  \/  ch ) )
32orcomd 719 1  |-  ( ph  ->  ( ch  \/  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 698
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 699
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  pm2.48  731  pm2.49  732  orim12i  749  pm1.5  755  animorr  814  animorlr  815  dcan  923  dcor  925  dcun  3518  exmidn0m  4179  regexmidlem1  4509  reg2exmidlema  4510  nn0suc  4580  nndceq0  4594  acexmidlem1  5837  nntri3or  6457  nntri2or2  6462  nndceq  6463  nndcel  6464  nnm00  6493  ssfilem  6837  diffitest  6849  tridc  6861  finexdc  6864  fientri3  6876  unsnfidcex  6881  unsnfidcel  6882  fidcenumlemrks  6914  fidcenumlemrk  6915  nninfisollemne  7091  nninfisol  7093  finomni  7100  exmidfodomrlemeldju  7151  exmidfodomrlemreseldju  7152  exmidfodomrlemr  7154  exmidfodomrlemrALT  7155  exmidaclem  7160  exmidontriimlem2  7174  mullocprlem  7507  recexprlemloc  7568  gt0ap0  8520  ltap  8527  recexaplem2  8545  nn1m1nn  8871  nn1gt1  8887  ltpnf  9712  mnflt  9715  xrltso  9728  xnn0dcle  9734  xnn0letri  9735  xrpnfdc  9774  xrmnfdc  9775  exfzdc  10171  apbtwnz  10205  expnnval  10454  exp0  10455  bc0k  10665  bcpasc  10675  xrmaxadd  11198  sumdc  11295  zsumdc  11321  fsum3  11324  fisumss  11329  isumss2  11330  fsumsplit  11344  zproddc  11516  fprodseq  11520  fprodssdc  11527  fprodsplitdc  11533  fprodsplit  11534  fprodunsn  11541  fprodcl2lem  11542  infssuzex  11878  pclemdc  12216  sumhashdc  12273  1arith  12293  ctiunctlemudc  12366  suplociccreex  13202  lgsdir2lem5  13533  djurclALT  13643  bj-nn0suc0  13792  trilpolemres  13881  trirec0  13883  nconstwlpolem  13903
  Copyright terms: Public domain W3C validator