![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > syl222anc | Structured version 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 |
![]() ![]() ![]() ![]() ![]() ![]() |
sylXanc.6 |
![]() ![]() ![]() ![]() ![]() ![]() |
syl222anc.7 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
syl222anc |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylXanc.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | sylXanc.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | sylXanc.3 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
4 | sylXanc.4 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
5 | sylXanc.5 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
6 | sylXanc.6 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 5, 6 | jca 532 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | syl222anc.7 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
9 | 1, 2, 3, 4, 7, 8 | syl221anc 1230 |
1
![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() |
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 185 df-an 371 df-3an 967 |
This theorem is referenced by: 3anandis 1321 3anandirs 1322 omopth2 7136 omeu 7137 dfac12lem2 8427 xaddass2 11327 xpncan 11328 divdenle 13948 pockthlem 14087 znidomb 18122 ang180lem5 22345 isosctrlem3 22354 log2tlbnd 22476 axcontlem8 23389 xlt2addrd 26222 xrge0addass 26316 xrge0npcan 26322 congmul 29478 jm2.25lem1 29515 jm2.26 29519 jm2.27a 29522 stoweidlem42 30005 4atexlemntlpq 34070 4atexlemnclw 34072 trlval2 34165 cdleme0moN 34227 cdleme16b 34281 cdleme16c 34282 cdleme16d 34283 cdleme16e 34284 cdleme17c 34290 cdlemeda 34300 cdleme20h 34318 cdleme20j 34320 cdleme20l2 34323 cdleme21c 34329 cdleme21ct 34331 cdleme22aa 34341 cdleme22cN 34344 cdleme22d 34345 cdleme22e 34346 cdleme22eALTN 34347 cdleme23b 34352 cdleme25a 34355 cdleme25dN 34358 cdleme27N 34371 cdleme28a 34372 cdleme28b 34373 cdleme29ex 34376 cdleme32c 34445 cdleme42k 34486 cdlemg2cex 34593 cdlemg2idN 34598 cdlemg31c 34701 cdlemk5a 34837 cdlemk5 34838 |
Copyright terms: Public domain | W3C validator |