![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > syl221anc | Structured version Visualization 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 |
![]() ![]() ![]() ![]() ![]() ![]() |
syl221anc.6 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
syl221anc |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylXanc.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | sylXanc.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | sylXanc.3 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
4 | sylXanc.4 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | jca 535 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | sylXanc.5 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
7 | syl221anc.6 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
8 | 1, 2, 5, 6, 7 | syl211anc 1274 |
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 189 df-an 373 df-3an 987 |
This theorem is referenced by: syl222anc 1284 vtocldf 3097 f1oprswap 5854 dmdcand 10412 modmul12d 12144 modnegd 12145 modadd12d 12146 exprec 12313 splval2 12864 eulerthlem2 14730 fermltl 14732 odzdvds 14740 odzdvdsOLD 14746 efgredleme 17393 efgredlemc 17395 blssps 21439 blss 21440 metequiv2 21525 met1stc 21536 met2ndci 21537 metdstri 21868 metdstriOLD 21883 xlebnum 21996 caubl 22277 divcxp 23632 cxple2a 23644 cxplead 23666 cxplt2d 23671 cxple2d 23672 mulcxpd 23673 ang180 23743 wilthlem2 23994 lgslem4 24227 lgsvalmod 24243 lgsmod 24249 lgsdir2lem4 24254 lgsdirprm 24257 lgsne0 24261 lgseisen 24281 ax5seglem9 24967 xrsmulgzz 28440 heiborlem8 32150 cdlemd4 33767 cdleme15a 33840 cdleme17b 33853 cdleme25a 33920 cdleme25c 33922 cdleme25dN 33923 cdleme26ee 33927 tendococl 34339 tendodi1 34351 tendodi2 34352 cdlemi 34387 tendocan 34391 cdlemk5a 34402 cdlemk5 34403 cdlemk10 34410 cdlemk5u 34428 cdlemkfid1N 34488 pellexlem6 35678 rpexpmord 35796 acongeq 35833 jm2.25 35854 stoweidlem42 37903 stoweidlem51 37912 ldepspr 40319 |
Copyright terms: Public domain | W3C validator |