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 1375 imainss 5001 xpexr2m 5027 funeu2 5196 imadiflem 5249 fnop 5273 ssimaex 5529 isosolem 5774 acexmidlem2 5821 fnovex 5854 cnvoprab 6181 smores3 6240 freccllem 6349 riinerm 6553 pw1fin 6855 enq0sym 7352 peano5nnnn 7812 axcaucvglemres 7819 uzind3 9277 xrltnsym 9700 xsubge0 9785 0fz1 9947 seqf 10360 seq3f1oleml 10402 exp1 10425 expp1 10426 resqrexlemf1 10908 resqrexlemfp1 10909 clim2ser 11234 clim2ser2 11235 isermulc2 11237 summodclem3 11277 fisumss 11289 fsum3cvg3 11293 iserabs 11372 isumshft 11387 isumsplit 11388 geoisum1 11416 geoisum1c 11417 cvgratnnlemnexp 11421 cvgratz 11429 mertenslem2 11433 clim2prod 11436 clim2divap 11437 fprodseq 11480 prodssdc 11486 fprodssdc 11487 effsumlt 11589 efgt1p 11593 gcd0id 11862 lcmgcd 11954 lcmdvds 11955 lcmid 11956 isprm2lem 11992 ennnfonelemjn 12131 neipsm 12554 xmetpsmet 12769 comet 12899 metrest 12906 expcncf 12992 exmid1stab 13572 cvgcmp2nlemabs 13603 nconstwlpolem 13635 |
Copyright terms: Public domain | W3C validator |