![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > olc | Unicode version |
Description: Introduction of a disjunct. Axiom *1.3 of [WhiteheadRussell] p. 96. (Contributed by NM, 30-Aug-1993.) (Revised by NM, 31-Jan-2015.) |
Ref | Expression |
---|---|
olc |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 19 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | jaob 700 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | mpbi 144 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | simpri 112 |
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 105 ax-ia2 106 ax-io 699 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: oibabs 704 pm1.4 717 olci 722 pm2.07 727 pm2.46 729 biorf 734 pm1.5 755 pm2.41 766 pm4.78i 772 pm3.48 775 ordi 806 andi 808 pm4.72 813 stdcn 833 pm2.54dc 877 pm2.85dc 891 dcor 920 dedlemb 955 xoranor 1356 19.33 1461 hbor 1526 nford 1547 19.30dc 1607 19.43 1608 19.32r 1659 euor2 2058 mooran2 2073 r19.32r 2581 undif3ss 3342 undif4 3430 issod 4249 onsucelsucexmid 4453 sucprcreg 4472 0elnn 4540 acexmidlemph 5775 nntri3or 6397 swoord1 6466 swoord2 6467 exmidaclem 7081 addlocprlem 7367 nqprloc 7377 apreap 8373 zletric 9122 zlelttric 9123 zmulcl 9131 zdceq 9150 zdcle 9151 zdclt 9152 nn0lt2 9156 elnn1uz2 9428 mnflt 9599 mnfltpnf 9601 xrltso 9612 fzdcel 9851 fzm1 9911 qletric 10052 qlelttric 10053 qdceq 10055 nn0o1gt2 11638 bj-fadc 13131 decidin 13175 triap 13399 |
Copyright terms: Public domain | W3C validator |