ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  orci GIF 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 𝜑
Assertion
Ref Expression
orci (𝜑𝜓)

Proof of Theorem orci
StepHypRef Expression
1 orci.1 . 2 𝜑
2 orc 712 . 2 (𝜑 → (𝜑𝜓))
31, 2ax-mp 5 1 (𝜑𝜓)
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  3695  onsucelsucexmidlem1  4524  regexmidlemm  4528  nn0suc  4600  nndceq0  4614  0elnn  4615  acexmidlem2  5866  dcfi  6974  exmidaclem  7201  indpi  7329  sup3exmid  8900  nn1gt1  8939  nneoor  9341  mnfltpnf  9769  bcpasc  10727  dceqnconst  14456  nconstwlpolem0  14459
  Copyright terms: Public domain W3C validator