![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > syl311anc | 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 |
![]() ![]() ![]() ![]() ![]() ![]() |
syl311anc.6 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
syl311anc |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylXanc.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | sylXanc.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | sylXanc.3 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | 3jca 1134 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | sylXanc.4 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
6 | sylXanc.5 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
7 | syl311anc.6 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
8 | 4, 5, 6, 7 | syl3anc 1184 |
1
![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem is referenced by: syl312anc 1205 syl321anc 1206 syl313anc 1208 syl331anc 1209 pythagtrip 13167 nmolb2d 18709 nmoleub 18722 cvlcvr1 29826 4atlem12b 30097 dalawlem10 30366 dalawlem13 30369 dalawlem15 30371 osumcllem11N 30452 lhp2atne 30520 lhp2at0ne 30522 cdlemd 30693 ltrneq3 30694 cdleme7d 30732 cdlemeg49le 30997 cdleme 31046 cdlemg1a 31056 ltrniotavalbN 31070 cdlemg44 31219 cdlemk19 31355 cdlemk27-3 31393 cdlemk33N 31395 cdlemk34 31396 cdlemk49 31437 cdlemk53a 31441 cdlemk19u 31456 cdlemk56w 31459 dia2dimlem4 31554 dih1dimatlem0 31815 |
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 178 df-an 361 df-3an 938 |
Copyright terms: Public domain | W3C validator |