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 132 | . 2 |
3 | sylan2br.2 | . 2 | |
4 | 2, 3 | sylan2 284 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: syl2anbr 290 xordc1 1388 imainss 5026 xpexr2m 5052 funeu2 5224 imadiflem 5277 fnop 5301 ssimaex 5557 isosolem 5803 acexmidlem2 5850 fnovex 5886 cnvoprab 6213 smores3 6272 freccllem 6381 riinerm 6586 pw1fin 6888 enq0sym 7394 peano5nnnn 7854 axcaucvglemres 7861 uzind3 9325 xrltnsym 9750 xsubge0 9838 0fz1 10001 seqf 10417 seq3f1oleml 10459 exp1 10482 expp1 10483 resqrexlemf1 10972 resqrexlemfp1 10973 clim2ser 11300 clim2ser2 11301 isermulc2 11303 summodclem3 11343 fisumss 11355 fsum3cvg3 11359 iserabs 11438 isumshft 11453 isumsplit 11454 geoisum1 11482 geoisum1c 11483 cvgratnnlemnexp 11487 cvgratz 11495 mertenslem2 11499 clim2prod 11502 clim2divap 11503 fprodseq 11546 prodssdc 11552 fprodssdc 11553 effsumlt 11655 efgt1p 11659 gcd0id 11934 lcmgcd 12032 lcmdvds 12033 lcmid 12034 isprm2lem 12070 pcmpt 12295 ennnfonelemjn 12357 neipsm 12948 xmetpsmet 13163 comet 13293 metrest 13300 expcncf 13386 lgscllem 13702 lgsdir2 13728 lgsdirnn0 13742 lgsdinn0 13743 exmid1stab 14033 cvgcmp2nlemabs 14064 nconstwlpolem 14096 |
Copyright terms: Public domain | W3C validator |