New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > syl3anc | Unicode version |
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
Ref | Expression |
---|---|
sylXanc.1 | |
sylXanc.2 | |
sylXanc.3 | |
syl111anc.4 |
Ref | Expression |
---|---|
syl3anc |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylXanc.1 | . . 3 | |
2 | sylXanc.2 | . . 3 | |
3 | sylXanc.3 | . . 3 | |
4 | 1, 2, 3 | 3jca 1132 | . 2 |
5 | syl111anc.4 | . 2 | |
6 | 4, 5 | syl 15 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 w3a 934 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 |
This theorem depends on definitions: df-bi 177 df-an 360 df-3an 936 |
This theorem is referenced by: syl112anc 1186 syl121anc 1187 syl211anc 1188 syl113anc 1194 syl131anc 1195 syl311anc 1196 syld3an3 1227 3jaod 1246 mpd3an23 1279 rspc3ev 2965 sbciedf 3081 pw1equn 4331 pw1eqadj 4332 findsd 4410 nnsucelr 4428 ltfintri 4466 lenltfin 4469 ncfindi 4475 nnpw1ex 4484 tfin11 4493 tfindi 4496 tfinltfinlem1 4500 nnadjoinpw 4521 sfin112 4529 sfindbl 4530 sfintfin 4532 tfinnn 4534 sfinltfin 4535 sfin111 4536 vfinncvntnn 4548 vfinspsslem1 4550 vfinncsp 4554 phi11lem1 4595 fvopab4t 5385 composevalg 5817 trd 5921 pmfun 6015 elmapi 6016 ncdisjun 6136 ce2le 6232 lemuc1 6252 lecadd2 6265 spacind 6285 nchoicelem4 6290 nchoicelem6 6292 nchoicelem19 6305 nchoice 6306 dmfrec 6314 |
Copyright terms: Public domain | W3C validator |