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

Theorem orcd 685
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 666 . 2  |-  ( ps 
->  ( ps  \/  ch ) )
31, 2syl 14 1  |-  ( ph  ->  ( ps  \/  ch ) )
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-io 663
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  olcd  686  pm2.47  692  orim12i  709  dcor  877  undif3ss  3232  reg2exmidlema  4285  acexmidlem1  5539  poxp  5884  nntri2or2  6142  nnm00  6168  ssfilem  6410  diffitest  6421  fientri3  6435  unsnfidcex  6440  unsnfidcel  6441  nqprloc  6797  mullocprlem  6822  recexprlemloc  6883  ltxrlt  7245  zmulcl  8485  nn0lt2  8510  zeo  8533  xrltso  8947  apbtwnz  9356  expnegap0  9581
  Copyright terms: Public domain W3C validator