![]() |
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 8912 nn1gt1 8951 nneoor 9353 mnfltpnf 9783 bcpasc 10741 dceqnconst 14689 nconstwlpolem0 14692 |
Copyright terms: Public domain | W3C validator |