![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > sylanb | Unicode version |
Description: A syllogism inference. (Contributed by NM, 18-May-1994.) |
Ref | Expression |
---|---|
sylanb.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
sylanb.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
sylanb |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylanb.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | biimpi 120 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
3 | sylanb.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | sylan 283 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: syl2anb 291 anabsan 575 2exeu 2118 eqtr2 2196 pm13.181 2429 rmob 3055 disjne 3476 seex 4334 tron 4381 fssres 5390 funbrfvb 5557 funopfvb 5558 fvelrnb 5562 fvco 5585 fvimacnvi 5629 ffvresb 5678 funresdfunsnss 5718 fvtp2g 5724 fvtp2 5727 fnex 5737 funex 5738 1st2nd 6179 dftpos4 6261 nnmsucr 6486 nnmcan 6517 xpmapenlem 6846 fundmfibi 6935 sup3exmid 8910 nzadd 9301 peano5uzti 9357 fnn0ind 9365 uztrn2 9541 irradd 9642 xltnegi 9831 xaddnemnf 9853 xaddnepnf 9854 xaddcom 9857 xnegdi 9864 elioore 9908 uzsubsubfz1 10043 fzo1fzo0n0 10178 elfzonelfzo 10225 qbtwnxr 10253 faclbnd 10714 faclbnd3 10716 dvdsprime 12114 pcgcd 12320 restuni 13543 stoig 13544 cnnei 13603 tgioo 13917 divcnap 13926 lgsdi 14309 bj-indind 14544 |
Copyright terms: Public domain | W3C validator |