![]() |
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 666 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | mpbi 143 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | simpli 109 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-io 665 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: pm2.67-2 669 pm1.4 681 orci 685 orcd 687 orcs 689 pm2.45 692 biorfi 700 pm1.5 717 pm2.4 730 pm4.44 731 pm4.45 733 pm3.48 734 pm2.76 757 orabs 763 ordi 765 andi 767 pm4.72 772 biort 774 dcim 822 pm2.54dc 828 pm4.78i 846 pm2.85dc 849 dcor 881 pm5.71dc 907 dedlema 915 3mix1 1112 xoranor 1313 19.33 1418 hbor 1483 nford 1504 19.30dc 1563 19.43 1564 19.32r 1615 moor 2019 r19.32r 2514 ssun1 3163 undif3ss 3260 reuun1 3281 prmg 3561 opthpr 3616 issod 4146 elelsuc 4236 ordtri2or2exmidlem 4342 regexmidlem1 4349 nndceq 6260 nndcel 6261 swoord1 6321 swoord2 6322 addlocprlem 7094 msqge0 8093 mulge0 8096 ltleap 8107 nn1m1nn 8440 elnnz 8760 zletric 8794 zlelttric 8795 zmulcl 8803 zdceq 8822 zdcle 8823 zdclt 8824 ltpnf 9251 xrlttri3 9267 fzdcel 9454 qletric 9655 qlelttric 9656 qdceq 9658 hashfiv01gt1 10190 iisum 10775 nn0o1gt2 11183 bj-nn0suc0 11845 |
Copyright terms: Public domain | W3C validator |