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

Theorem orci 731
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 712 . 2  |-  ( ph  ->  ( ph  \/  ps ) )
31, 2ax-mp 5 1  |-  ( ph  \/  ps )
Colors of variables: wff set class
Syntax hints:    \/ wo 708
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-io 709
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  truorfal  1406  prid1g  3696  onsucelsucexmidlem1  4527  regexmidlemm  4531  nn0suc  4603  nndceq0  4617  0elnn  4618  acexmidlem2  5871  dcfi  6979  exmidaclem  7206  indpi  7340  sup3exmid  8913  nn1gt1  8952  nneoor  9354  mnfltpnf  9784  bcpasc  10745  dceqnconst  14777  nconstwlpolem0  14780
  Copyright terms: Public domain W3C validator