Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > orcd | Unicode version |
Description: Deduction introducing a disjunct. (Contributed by NM, 20-Sep-2007.) |
Ref | Expression |
---|---|
orcd.1 |
Ref | Expression |
---|---|
orcd |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | orcd.1 | . 2 | |
2 | orc 665 | . 2 | |
3 | 1, 2 | syl 14 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wo 661 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-io 662 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: olcd 685 pm2.47 691 orim12i 708 dcor 876 undif3ss 3225 reg2exmidlema 4277 acexmidlem1 5528 poxp 5873 nntri2or2 6099 nnm00 6125 ssfilem 6360 diffitest 6371 fientri3 6381 unsnfidcex 6385 unsnfidcel 6386 nqprloc 6735 mullocprlem 6760 recexprlemloc 6821 ltxrlt 7178 zmulcl 8404 nn0lt2 8429 zeo 8452 xrltso 8871 expnegap0 9484 |
Copyright terms: Public domain | W3C validator |