![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > orci | Unicode version |
Description: Deduction introducing a disjunct. (Contributed by NM, 19-Jan-2008.) (Revised by Mario Carneiro, 31-Jan-2015.) |
Ref | Expression |
---|---|
orci.1 |
![]() ![]() |
Ref | Expression |
---|---|
orci |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | orci.1 |
. 2
![]() ![]() | |
2 | orc 712 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ax-mp 5 |
1
![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() |
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 |