Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > syl32anc | Unicode version |
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
Ref | Expression |
---|---|
sylXanc.1 | |
sylXanc.2 | |
sylXanc.3 | |
sylXanc.4 | |
sylXanc.5 | |
syl32anc.6 |
Ref | Expression |
---|---|
syl32anc |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylXanc.1 | . 2 | |
2 | sylXanc.2 | . 2 | |
3 | sylXanc.3 | . 2 | |
4 | sylXanc.4 | . . 3 | |
5 | sylXanc.5 | . . 3 | |
6 | 4, 5 | jca 304 | . 2 |
7 | syl32anc.6 | . 2 | |
8 | 1, 2, 3, 6, 7 | syl31anc 1204 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 w3a 947 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 949 |
This theorem is referenced by: ioom 10006 modifeq2int 10127 modaddmodup 10128 seq3f1olemqsum 10241 seq3f1o 10245 exple1 10317 leexp2rd 10422 facubnd 10459 permnn 10485 dfabsmax 10957 expcnvre 11240 dvdsadd2b 11467 dvdsmulgcd 11640 sqgcd 11644 bezoutr 11647 cncongr2 11712 pw2dvds 11771 hashgcdlem 11830 tgioo 12642 |
Copyright terms: Public domain | W3C validator |