![]() |
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 710 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | mpbi 145 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | simpri 113 |
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-ia2 107 ax-io 709 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: oibabs 714 pm1.4 727 olci 732 pm2.07 737 pm2.46 739 biorf 744 pm1.5 765 pm2.41 776 pm4.78i 782 pm3.48 785 ordi 816 andi 818 pm4.72 827 stdcn 847 pm2.54dc 891 pm2.85dc 905 dcor 935 dedlemb 970 xoranor 1377 19.33 1484 hbor 1546 nford 1567 19.30dc 1627 19.43 1628 19.32r 1680 euor2 2084 mooran2 2099 r19.32r 2623 undif3ss 3396 undif4 3485 issod 4319 onsucelsucexmid 4529 sucprcreg 4548 0elnn 4618 acexmidlemph 5867 nntri3or 6493 swoord1 6563 swoord2 6564 exmidaclem 7206 exmidontri2or 7241 addlocprlem 7533 nqprloc 7543 apreap 8542 zletric 9295 zlelttric 9296 zmulcl 9304 zdceq 9326 zdcle 9327 zdclt 9328 nn0lt2 9332 elnn1uz2 9605 mnflt 9781 mnfltpnf 9783 xrltso 9794 fzdcel 10037 fzm1 10097 qletric 10241 qlelttric 10242 qdceq 10244 qsqeqor 10627 nn0o1gt2 11904 prm23lt5 12257 bj-fadc 14388 decidin 14431 triap 14659 tridceq 14686 |
Copyright terms: Public domain | W3C validator |