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

Theorem orci 705
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 686 . 2  |-  ( ph  ->  ( ph  \/  ps ) )
31, 2ax-mp 5 1  |-  ( ph  \/  ps )
Colors of variables: wff set class
Syntax hints:    \/ wo 682
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-io 683
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  truorfal  1369  prid1g  3597  onsucelsucexmidlem1  4413  regexmidlemm  4417  nn0suc  4488  nndceq0  4501  0elnn  4502  acexmidlem2  5739  exmidaclem  7032  indpi  7118  sup3exmid  8683  nn1gt1  8722  nneoor  9121  mnfltpnf  9539  bcpasc  10480
  Copyright terms: Public domain W3C validator