![]() |
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 284 |
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 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: syl2anb 289 dcor 920 bm1.1 2125 eqtr3 2160 elnelne1 2413 elnelne2 2414 morex 2872 reuss2 3361 reupick 3365 rabsneu 3604 opabss 4000 triun 4047 poirr 4237 wepo 4289 wetrep 4290 rexxfrd 4392 reg3exmidlemwe 4501 nnsuc 4537 fnfco 5305 fun11iun 5396 fnressn 5614 fvpr1g 5634 fvtp1g 5636 fvtp3g 5638 fvtp3 5641 f1mpt 5680 caovlem2d 5971 offval 5997 dfoprab3 6097 1stconst 6126 2ndconst 6127 poxp 6137 tfrlemisucaccv 6230 tfr1onlemsucaccv 6246 tfrcllemsucaccv 6259 fiintim 6825 addclpi 7159 addnidpig 7168 reapmul1 8381 nnnn0addcl 9031 un0addcl 9034 un0mulcl 9035 zltnle 9124 nn0ge0div 9162 uzind3 9188 uzind4 9410 ltsubrp 9507 ltaddrp 9508 xrlttr 9611 xrltso 9612 xltnegi 9648 xaddnemnf 9670 xaddnepnf 9671 xaddcom 9674 xnegdi 9681 xsubge0 9694 fzind2 10047 qltnle 10054 qbtwnxr 10066 exp3vallem 10325 expp1 10331 expnegap0 10332 expcllem 10335 mulexpzap 10364 expaddzap 10368 expmulzap 10370 hashunlem 10582 shftf 10634 sqrtdiv 10846 mulcn2 11113 summodclem2 11183 fsum3 11188 cvgratz 11333 prodmodclem2 11378 zproddc 11380 dvdsflip 11585 dvdsfac 11594 lcmgcdlem 11794 rpexp1i 11868 hashdvds 11933 hashgcdlem 11939 lmss 12454 xmetrtri 12584 blssioo 12753 divcnap 12763 dedekindicc 12819 dvidlemap 12868 dvrecap 12885 dveflem 12895 bj-bdfindes 13318 bj-findes 13350 |
Copyright terms: Public domain | W3C validator |