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

Theorem orcd 705
Description: Deduction introducing a disjunct. (Contributed by NM, 20-Sep-2007.)
Hypothesis
Ref Expression
orcd.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
orcd  |-  ( ph  ->  ( ps  \/  ch ) )

Proof of Theorem orcd
StepHypRef Expression
1 orcd.1 . 2  |-  ( ph  ->  ps )
2 orc 684 . 2  |-  ( ps 
->  ( ps  \/  ch ) )
31, 2syl 14 1  |-  ( ph  ->  ( ps  \/  ch ) )
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-io 681
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  olcd  706  pm2.47  712  orim12i  731  dcor  902  undif3ss  3305  dcun  3441  exmidn0m  4092  exmidsssn  4093  reg2exmidlema  4417  acexmidlem1  5736  poxp  6095  nntri2or2  6360  nnm00  6391  ssfilem  6735  diffitest  6747  tridc  6759  finexdc  6762  fientri3  6769  unsnfidcex  6774  unsnfidcel  6775  fidcenumlemrks  6807  finomni  6978  exmidfodomrlemeldju  7019  exmidfodomrlemreseldju  7020  exmidfodomrlemr  7022  exmidfodomrlemrALT  7023  exmidaclem  7028  nqprloc  7317  mullocprlem  7342  recexprlemloc  7403  ltxrlt  7794  zmulcl  9061  nn0lt2  9086  zeo  9110  xrltso  9533  apbtwnz  9998  expnegap0  10252  xrmaxadd  10981  zsumdc  11104  fsumsplit  11127  sumsplitdc  11152  isumlessdc  11216  suplociccreex  12677  djulclALT  12842  trilpolemres  13069
  Copyright terms: Public domain W3C validator