Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > sylan2br | Unicode version |
Description: A syllogism inference. (Contributed by NM, 21-Apr-1994.) |
Ref | Expression |
---|---|
sylan2br.1 | |
sylan2br.2 |
Ref | Expression |
---|---|
sylan2br |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylan2br.1 | . . 3 | |
2 | 1 | biimpri 124 | . 2 |
3 | sylan2br.2 | . 2 | |
4 | 2, 3 | sylan2 270 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 97 wb 98 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: syl2anbr 276 xordc1 1284 imainss 4739 xpexr2m 4762 funeu2 4927 imadiflem 4978 fnop 5002 ssimaex 5234 isosolem 5463 acexmidlem2 5509 fnovex 5538 smores3 5908 riinerm 6179 enq0sym 6530 peano5nnnn 6966 axcaucvglemres 6973 uzind3 8351 xrltnsym 8714 0fz1 8909 iseqf 9224 expivallem 9256 expival 9257 exp1 9261 expp1 9262 resqrexlemf1 9606 resqrexlemfp1 9607 clim2iser 9857 clim2iser2 9858 iisermulc2 9860 iserile 9862 climserile 9865 |
Copyright terms: Public domain | W3C validator |