![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > sylan2b | Unicode version |
Description: A syllogism inference. (Contributed by NM, 21-Apr-1994.) |
Ref | Expression |
---|---|
sylan2b.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
sylan2b.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
sylan2b |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylan2b.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | biimpi 119 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
3 | sylan2b.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | sylan2 281 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: syl2anb 286 dcor 882 bm1.1 2074 eqtr3 2108 morex 2802 reuss2 3282 reupick 3286 rabsneu 3521 opabss 3910 triun 3957 poirr 4145 wepo 4197 wetrep 4198 rexxfrd 4300 reg3exmidlemwe 4409 nnsuc 4445 fnfco 5200 fun11iun 5289 fnressn 5499 fvpr1g 5519 fvtp1g 5521 fvtp3g 5523 fvtp3 5526 f1mpt 5566 caovlem2d 5853 offval 5879 dfoprab3 5977 1stconst 6002 2ndconst 6003 poxp 6013 tfrlemisucaccv 6106 tfr1onlemsucaccv 6122 tfrcllemsucaccv 6135 fiintim 6695 addclpi 6949 addnidpig 6958 reapmul1 8135 nnnn0addcl 8766 un0addcl 8769 un0mulcl 8770 zltnle 8859 nn0ge0div 8896 uzind3 8922 uzind4 9139 ltsubrp 9231 ltaddrp 9232 xrlttr 9328 xrltso 9329 xltnegi 9360 fzind2 9713 qltnle 9720 qbtwnxr 9732 exp3vallem 10019 expp1 10025 expnegap0 10026 expcllem 10029 mulexpzap 10058 expaddzap 10062 expmulzap 10064 hashunlem 10275 shftf 10327 sqrtdiv 10538 mulcn2 10764 isummolem2 10835 cvgratz 10989 dvdsflip 11193 dvdsfac 11202 lcmgcdlem 11400 rpexp1i 11474 hashdvds 11538 hashgcdlem 11544 bj-bdfindes 12148 bj-findes 12180 |
Copyright terms: Public domain | W3C validator |