![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > sylcom | Unicode version |
Description: Syllogism inference with commutation of antecedents. (Contributed by NM, 29-Aug-2004.) (Proof shortened by Mel L. O'Cat, 2-Feb-2006.) (Proof shortened by Stefan Allan, 23-Feb-2006.) |
Ref | Expression |
---|---|
sylcom.1 | |
sylcom.2 |
Ref | Expression |
---|---|
sylcom |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylcom.1 | . 2 | |
2 | sylcom.2 | . . 3 | |
3 | 2 | a2i 13 | . 2 |
4 | 1, 3 | syl 16 | 1 |
Colors of variables: wff setvar class |
Syntax hints: -> wi 4 |
This theorem is referenced by: syl5com 30 syl6 33 syli 37 mpbidi 216 2eu6 2383 dmcosseq 5269 iss 5326 funopg 5625 limuni3 6687 frxp 6910 tz7.49 7129 dif1enOLD 7772 dif1en 7773 enp1i 7775 frfi 7785 unblem3 7794 isfinite2 7798 iunfi 7828 tcrank 8323 infdif 8610 isf34lem6 8781 axdc3lem4 8854 suplem1pr 9451 uzwo 11173 uzwoOLD 11174 gsumcom2 17003 cmpsublem 19899 nrmhaus 20327 metrest 21027 finiunmbl 21954 wilthlem3 23344 cusgrafi 24482 clwwlkn0 24774 h1datomi 26499 chirredlem1 27309 mclsax 28929 wfrlem12 29354 frrlem11 29399 lineext 29726 onsucconi 29902 sdclem2 30235 heibor1lem 30305 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 |
Copyright terms: Public domain | W3C validator |