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

Theorem orci 703
Description: Deduction introducing a disjunct. (Contributed by NM, 19-Jan-2008.) (Revised by Mario Carneiro, 31-Jan-2015.)
Hypothesis
Ref Expression
orci.1  |-  ph
Assertion
Ref Expression
orci  |-  ( ph  \/  ps )

Proof of Theorem orci
StepHypRef Expression
1 orci.1 . 2  |-  ph
2 orc 684 . 2  |-  ( ph  ->  ( ph  \/  ps ) )
31, 2ax-mp 5 1  |-  ( ph  \/  ps )
Colors of variables: wff set class
Syntax hints:    \/ 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:  truorfal  1367  prid1g  3595  onsucelsucexmidlem1  4411  regexmidlemm  4415  nn0suc  4486  nndceq0  4499  0elnn  4500  acexmidlem2  5737  exmidaclem  7028  indpi  7114  sup3exmid  8672  nn1gt1  8711  nneoor  9104  mnfltpnf  9511  bcpasc  10452
  Copyright terms: Public domain W3C validator