![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > orc | Unicode version |
Description: Introduction of a disjunct. Theorem *2.2 of [WhiteheadRussell] p. 104. (Contributed by NM, 30-Aug-1993.) (Revised by NM, 31-Jan-2015.) |
Ref | Expression |
---|---|
orc |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 19 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | jaob 711 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | mpbi 145 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | simpli 111 |
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 710 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: pm2.67-2 714 pm1.4 728 orci 732 orcd 734 orcs 736 pm2.45 739 biorfi 747 pm1.5 766 pm2.4 779 pm4.44 780 pm4.78i 783 pm4.45 785 pm3.48 786 pm2.76 809 orabs 815 ordi 817 andi 819 pm4.72 828 biort 830 dcim 842 pm2.54dc 892 pm2.85dc 906 dcor 937 pm5.71dc 963 dedlema 971 3mix1 1168 xoranor 1388 19.33 1495 hbor 1557 nford 1578 19.30dc 1638 19.43 1639 19.32r 1691 moor 2109 r19.32r 2636 ssun1 3313 undif3ss 3411 reuun1 3432 prmg 3728 opthpr 3787 exmidn0m 4219 issod 4337 elelsuc 4427 ordtri2or2exmidlem 4543 regexmidlem1 4550 nndceq 6524 nndcel 6525 swoord1 6588 swoord2 6589 exmidontri2or 7272 addlocprlem 7564 msqge0 8603 mulge0 8606 ltleap 8619 nn1m1nn 8967 elnnz 9293 zletric 9327 zlelttric 9328 zmulcl 9336 zdceq 9358 zdcle 9359 zdclt 9360 ltpnf 9810 xrlttri3 9827 xrpnfdc 9872 xrmnfdc 9873 fzdcel 10070 qletric 10274 qlelttric 10275 qdceq 10277 qsqeqor 10662 hashfiv01gt1 10794 isum 11425 iprodap 11620 iprodap0 11622 nn0o1gt2 11942 prm23lt5 12295 4sqlem17 12439 bj-trdc 14962 bj-nn0suc0 15160 triap 15236 tridceq 15263 |
Copyright terms: Public domain | W3C validator |