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 701 | . 2 | |
3 | 1, 2 | syl 14 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wo 697 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-io 698 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: olcd 723 pm2.47 729 orim12i 748 dcor 919 undif3ss 3337 dcun 3473 exmidn0m 4124 exmidsssn 4125 reg2exmidlema 4449 acexmidlem1 5770 poxp 6129 nntri2or2 6394 nnm00 6425 ssfilem 6769 diffitest 6781 tridc 6793 finexdc 6796 fientri3 6803 unsnfidcex 6808 unsnfidcel 6809 fidcenumlemrks 6841 finomni 7012 exmidfodomrlemeldju 7055 exmidfodomrlemreseldju 7056 exmidfodomrlemr 7058 exmidfodomrlemrALT 7059 exmidaclem 7064 nqprloc 7356 mullocprlem 7381 recexprlemloc 7442 ltxrlt 7833 zmulcl 9110 nn0lt2 9135 zeo 9159 xrltso 9585 apbtwnz 10050 expnegap0 10304 xrmaxadd 11033 zsumdc 11156 fsumsplit 11179 sumsplitdc 11204 isumlessdc 11268 suplociccreex 12774 djulclALT 13011 trilpolemres 13238 |
Copyright terms: Public domain | W3C validator |