Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > syl133anc | Structured version Visualization version Unicode version |
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
Ref | Expression |
---|---|
syl12anc.1 | |
syl12anc.2 | |
syl12anc.3 | |
syl22anc.4 | |
syl23anc.5 | |
syl33anc.6 | |
syl133anc.7 | |
syl133anc.8 |
Ref | Expression |
---|---|
syl133anc |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl12anc.1 | . 2 | |
2 | syl12anc.2 | . 2 | |
3 | syl12anc.3 | . 2 | |
4 | syl22anc.4 | . 2 | |
5 | syl23anc.5 | . . 3 | |
6 | syl33anc.6 | . . 3 | |
7 | syl133anc.7 | . . 3 | |
8 | 5, 6, 7 | 3jca 1242 | . 2 |
9 | syl133anc.8 | . 2 | |
10 | 1, 2, 3, 4, 8, 9 | syl131anc 1339 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 w3a 1037 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 197 df-an 386 df-3an 1039 |
This theorem is referenced by: syl233anc 1355 mdetuni0 20427 frgrwopreg 27187 cgrtr4d 32092 cgrtrand 32100 cgrtr3and 32102 cgrcoml 32103 cgrextendand 32116 segconeu 32118 btwnouttr2 32129 cgr3tr4 32159 cgrxfr 32162 btwnxfr 32163 lineext 32183 brofs2 32184 brifs2 32185 fscgr 32187 btwnconn1lem2 32195 btwnconn1lem4 32197 btwnconn1lem8 32201 btwnconn1lem11 32204 brsegle2 32216 seglecgr12im 32217 segletr 32221 outsidele 32239 dalem13 34962 2llnma1b 35072 cdlemblem 35079 cdlemb 35080 lhpexle3 35298 lhpat 35329 4atex2-0bOLDN 35365 cdlemd4 35488 cdleme14 35560 cdleme19b 35592 cdleme20f 35602 cdleme20j 35606 cdleme20k 35607 cdleme20l2 35609 cdleme20 35612 cdleme22a 35628 cdleme22e 35632 cdleme26e 35647 cdleme28 35661 cdleme38n 35752 cdleme41sn4aw 35763 cdleme41snaw 35764 cdlemg6c 35908 cdlemg6 35911 cdlemg8c 35917 cdlemg9 35922 cdlemg10a 35928 cdlemg12c 35933 cdlemg12d 35934 cdlemg18d 35969 cdlemg18 35970 cdlemg20 35973 cdlemg21 35974 cdlemg22 35975 cdlemg28a 35981 cdlemg33b0 35989 cdlemg28b 35991 cdlemg33a 35994 cdlemg33 35999 cdlemg34 36000 cdlemg36 36002 cdlemg38 36003 cdlemg46 36023 cdlemk6 36125 cdlemki 36129 cdlemksv2 36135 cdlemk11 36137 cdlemk6u 36150 cdleml4N 36267 cdlemn11pre 36499 |
Copyright terms: Public domain | W3C validator |