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: wi 4 wa 103 wo 698 |
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 817 stdcn 837 pm2.54dc 881 pm2.85dc 895 dcor 924 dedlemb 959 xoranor 1366 19.33 1471 hbor 1533 nford 1554 19.30dc 1614 19.43 1615 19.32r 1667 euor2 2071 mooran2 2086 r19.32r 2610 undif3ss 3378 undif4 3466 issod 4291 onsucelsucexmid 4501 sucprcreg 4520 0elnn 4590 acexmidlemph 5829 nntri3or 6452 swoord1 6521 swoord2 6522 exmidaclem 7155 exmidontri2or 7190 addlocprlem 7467 nqprloc 7477 apreap 8476 zletric 9226 zlelttric 9227 zmulcl 9235 zdceq 9257 zdcle 9258 zdclt 9259 nn0lt2 9263 elnn1uz2 9536 mnflt 9710 mnfltpnf 9712 xrltso 9723 fzdcel 9965 fzm1 10025 qletric 10169 qlelttric 10170 qdceq 10172 nn0o1gt2 11827 prm23lt5 12174 bj-fadc 13474 decidin 13519 triap 13749 tridceq 13776 |
Copyright terms: Public domain | W3C validator |