![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > syli | Unicode version |
Description: Syllogism inference with common nested antecedent. (Contributed by NM, 4-Nov-2004.) |
Ref | Expression |
---|---|
syli.1 | |
syli.2 |
Ref | Expression |
---|---|
syli |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syli.1 | . 2 | |
2 | syli.2 | . . 3 | |
3 | 2 | com12 31 | . 2 |
4 | 1, 3 | sylcom 29 | 1 |
Colors of variables: wff setvar class |
Syntax hints: -> wi 4 |
This theorem is referenced by: ibd 243 bija 355 equvini 2087 equveli 2088 equveliOLD 2089 2eu6 2383 rgen2a 2884 rexraleqim 3225 elreldm 5232 tz6.12c 5890 onminex 6642 rntpos 6987 smores 7042 seqomlem2 7135 f1domg 7555 php 7721 fodomnum 8459 carduniima 8498 cardmin 8960 negn0 11197 sqrmo 13085 grpomndo 25348 elghomlem2OLD 25364 isch3 26159 cgrtriv 29652 wl-lem-moexsb 30017 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 |
Copyright terms: Public domain | W3C validator |