New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > sylancl | Unicode version |
Description: Syllogism inference combined with modus ponens. (Contributed by Jeff Madsen, 2-Sep-2009.) |
Ref | Expression |
---|---|
sylancl.1 | |
sylancl.2 | |
sylancl.3 |
Ref | Expression |
---|---|
sylancl |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylancl.1 | . 2 | |
2 | sylancl.2 | . . 3 | |
3 | 2 | a1i 10 | . 2 |
4 | sylancl.3 | . 2 | |
5 | 1, 3, 4 | syl2anc 642 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wa 358 |
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 177 df-an 360 |
This theorem is referenced by: equveli 1988 syl5sseq 3319 ssdifin0 3631 uneqdifeq 3638 unimax 3925 pw1exg 4302 cokexg 4309 pwexg 4328 nnsucelr 4428 vfinspnn 4541 isoini2 5498 fullfunexg 5859 qsexg 5982 mapsn 6026 enrflxg 6034 cnven 6045 ncdisjun 6136 addccan2nclem2 6264 nncdiv3 6277 nnc3n3p1 6278 nnc3n3p2 6279 nchoicelem1 6289 nchoicelem2 6290 nchoicelem12 6300 frec0 6321 |
Copyright terms: Public domain | W3C validator |