![]() |
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 133 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
3 | sylan2br.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | sylan2 286 |
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: syl2anbr 292 xordc1 1393 exmid1stab 4208 imainss 5044 xpexr2m 5070 funeu2 5242 imadiflem 5295 fnop 5319 ssimaex 5577 isosolem 5824 acexmidlem2 5871 fnovex 5907 cnvoprab 6234 smores3 6293 freccllem 6402 riinerm 6607 pw1fin 6909 enq0sym 7430 peano5nnnn 7890 axcaucvglemres 7897 uzind3 9364 xrltnsym 9791 xsubge0 9879 0fz1 10042 seqf 10458 seq3f1oleml 10500 exp1 10523 expp1 10524 resqrexlemf1 11012 resqrexlemfp1 11013 clim2ser 11340 clim2ser2 11341 isermulc2 11343 summodclem3 11383 fisumss 11395 fsum3cvg3 11399 iserabs 11478 isumshft 11493 isumsplit 11494 geoisum1 11522 geoisum1c 11523 cvgratnnlemnexp 11527 cvgratz 11535 mertenslem2 11539 clim2prod 11542 clim2divap 11543 fprodseq 11586 prodssdc 11592 fprodssdc 11593 effsumlt 11695 efgt1p 11699 gcd0id 11974 lcmgcd 12072 lcmdvds 12073 lcmid 12074 isprm2lem 12110 pcmpt 12335 ennnfonelemjn 12397 mulg1 12944 srglmhm 13129 srgrmhm 13130 neipsm 13547 xmetpsmet 13762 comet 13892 metrest 13899 expcncf 13985 lgscllem 14301 lgsdir2 14327 lgsdirnn0 14341 lgsdinn0 14342 cvgcmp2nlemabs 14662 nconstwlpolem 14694 |
Copyright terms: Public domain | W3C validator |