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 699 | . . 3 | |
3 | 1, 2 | mpbi 144 | . 2 |
4 | 3 | simpri 112 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 wo 697 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-io 698 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: oibabs 703 pm1.4 716 olci 721 pm2.07 726 pm2.46 728 biorf 733 pm1.5 754 pm2.41 765 pm4.78i 771 pm3.48 774 ordi 805 andi 807 pm4.72 812 stdcn 832 pm2.54dc 876 pm2.85dc 890 dcor 919 dedlemb 954 xoranor 1355 19.33 1460 hbor 1525 nford 1546 19.30dc 1606 19.43 1607 19.32r 1658 euor2 2055 mooran2 2070 r19.32r 2576 undif3ss 3332 undif4 3420 issod 4236 onsucelsucexmid 4440 sucprcreg 4459 0elnn 4527 acexmidlemph 5760 nntri3or 6382 swoord1 6451 swoord2 6452 exmidaclem 7057 addlocprlem 7336 nqprloc 7346 apreap 8342 zletric 9091 zlelttric 9092 zmulcl 9100 zdceq 9119 zdcle 9120 zdclt 9121 nn0lt2 9125 elnn1uz2 9394 mnflt 9562 mnfltpnf 9564 xrltso 9575 fzdcel 9813 fzm1 9873 qletric 10014 qlelttric 10015 qdceq 10017 nn0o1gt2 11591 bj-fadc 12949 decidin 12993 triap 13213 |
Copyright terms: Public domain | W3C validator |