Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > syl323anc | 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 | |
syl233anc.8 | |
syl323anc.9 |
Ref | Expression |
---|---|
syl323anc |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl12anc.1 | . 2 | |
2 | syl12anc.2 | . 2 | |
3 | syl12anc.3 | . 2 | |
4 | syl22anc.4 | . . 3 | |
5 | syl23anc.5 | . . 3 | |
6 | 4, 5 | jca 554 | . 2 |
7 | syl33anc.6 | . 2 | |
8 | syl133anc.7 | . 2 | |
9 | syl233anc.8 | . 2 | |
10 | syl323anc.9 | . 2 | |
11 | 1, 2, 3, 6, 7, 8, 9, 10 | syl313anc 1350 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wa 384 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: 4atlem11 34895 dalem52 35010 dath2 35023 dalawlem1 35157 dalaw 35172 cdlemb2 35327 4atexlem7 35361 cdleme7ga 35535 cdleme18a 35578 cdleme18c 35580 cdleme21f 35620 cdleme26f2ALTN 35652 cdleme26f2 35653 cdleme27a 35655 cdlemg17dN 35951 cdlemg18a 35966 cdlemg31d 35988 cdlemg48 36025 cdlemj1 36109 dihord4 36547 |
Copyright terms: Public domain | W3C validator |