Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 3jaod | Unicode version |
Description: Disjunction of 3 antecedents (deduction). (Contributed by NM, 14-Oct-2005.) |
Ref | Expression |
---|---|
3jaod.1 | |
3jaod.2 | |
3jaod.3 |
Ref | Expression |
---|---|
3jaod |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3jaod.1 | . 2 | |
2 | 3jaod.2 | . 2 | |
3 | 3jaod.3 | . 2 | |
4 | 3jao 1279 | . 2 | |
5 | 1, 2, 3, 4 | syl3anc 1216 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 w3o 961 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 698 |
This theorem depends on definitions: df-bi 116 df-3or 963 df-3an 964 |
This theorem is referenced by: 3jaodan 1284 3jaao 1286 issod 4241 nnawordex 6424 addlocprlem 7346 nqprloc 7356 ltexprlemrl 7421 aptiprleml 7450 aptiprlemu 7451 elnn0z 9070 zaddcl 9097 zletric 9101 zlelttric 9102 zltnle 9103 zdceq 9129 zdcle 9130 zdclt 9131 nn01to3 9412 xposdif 9668 fzdcel 9823 qletric 10024 qlelttric 10025 qltnle 10026 qdceq 10027 frec2uzlt2d 10180 triap 13227 |
Copyright terms: Public domain | W3C validator |