Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > syl13anc | Unicode version |
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
Ref | Expression |
---|---|
sylXanc.1 | |
sylXanc.2 | |
sylXanc.3 | |
sylXanc.4 | |
syl13anc.5 |
Ref | Expression |
---|---|
syl13anc |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylXanc.1 | . 2 | |
2 | sylXanc.2 | . . 3 | |
3 | sylXanc.3 | . . 3 | |
4 | sylXanc.4 | . . 3 | |
5 | 2, 3, 4 | 3jca 1118 | . 2 |
6 | syl13anc.5 | . 2 | |
7 | 1, 5, 6 | syl2anc 403 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 102 w3a 919 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 df-3an 921 |
This theorem is referenced by: syl23anc 1176 syl33anc 1184 caovassd 5680 caovcand 5683 caovordid 5687 caovordd 5689 caovdid 5696 caovdird 5699 swoer 6157 swoord1 6158 swoord2 6159 suplub2ti 6414 prarloclem3 6687 fzosubel3 9205 iseqsplit 9458 iseqcaopr 9462 divalglemex 10322 |
Copyright terms: Public domain | W3C validator |