![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > olcd | Unicode version |
Description: Deduction introducing a disjunct. (Contributed by NM, 11-Apr-2008.) (Proof shortened by Wolf Lammen, 3-Oct-2013.) |
Ref | Expression |
---|---|
orcd.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
olcd |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | orcd.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | orcd 651 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | orcomd 647 |
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 99 ax-ia2 100 ax-ia3 101 ax-io 629 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: pm2.48 659 pm2.49 660 orim12i 675 pm1.5 681 dcan 841 dcor 842 sspsstrir 3040 regexmidlem1 4218 nn0suc 4270 nndceq0 4282 acexmidlem1 5451 nntri3or 6011 nndceq 6015 nndcel 6016 nnm00 6038 ssfiexmid 6254 mullocprlem 6551 recexprlemloc 6603 gt0ap0 7408 recexaplem2 7415 nn1m1nn 7713 nn1gt1 7728 ltpnf 8472 mnflt 8474 xrltso 8487 expinnval 8912 exp0 8913 bj-nn0suc0 9410 |
Copyright terms: Public domain | W3C validator |