![]() |
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 120 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
3 | sylan2b.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: syl2anb 291 dcor 937 bm1.1 2174 eqtr3 2209 elnelne1 2464 elnelne2 2465 morex 2936 reuss2 3430 reupick 3434 rabsneu 3680 opabss 4082 triun 4129 poirr 4325 wepo 4377 wetrep 4378 rexxfrd 4481 reg3exmidlemwe 4596 nnsuc 4633 fnfco 5409 fun11iun 5501 fnressn 5723 fvpr1g 5743 fvtp1g 5745 fvtp3g 5747 fvtp3 5750 f1mpt 5793 caovlem2d 6089 offval 6114 dfoprab3 6216 1stconst 6246 2ndconst 6247 poxp 6257 tfrlemisucaccv 6350 tfr1onlemsucaccv 6366 tfrcllemsucaccv 6379 fiintim 6957 addclpi 7356 addnidpig 7365 reapmul1 8582 nnnn0addcl 9236 un0addcl 9239 un0mulcl 9240 zltnle 9329 nn0ge0div 9370 uzind3 9396 uzind4 9618 ltsubrp 9720 ltaddrp 9721 xrlttr 9825 xrltso 9826 xltnegi 9865 xaddnemnf 9887 xaddnepnf 9888 xaddcom 9891 xnegdi 9898 xsubge0 9911 fzind2 10269 qltnle 10276 qbtwnxr 10288 exp3vallem 10552 expp1 10558 expnegap0 10559 expcllem 10562 mulexpzap 10591 expaddzap 10595 expmulzap 10597 hashunlem 10816 shftf 10871 sqrtdiv 11083 mulcn2 11352 summodclem2 11422 fsum3 11427 cvgratz 11572 prodmodclem2 11617 zproddc 11619 prodsnf 11632 dvdsflip 11889 dvdsfac 11898 lcmgcdlem 12109 rpexp1i 12186 hashdvds 12253 hashgcdlem 12270 phisum 12272 pcqcl 12338 pcid 12356 ssnnctlemct 12497 issubmd 12926 grpinvnzcl 13016 mulgneg 13080 mulgnn0z 13089 01eq0ring 13536 lmss 14203 xmetrtri 14333 blssioo 14502 divcnap 14512 dedekindicc 14568 dvidlemap 14617 dvrecap 14634 dveflem 14644 lgsval3 14877 lgsdir2 14892 2sqlem6 14925 bj-bdfindes 15159 bj-findes 15191 |
Copyright terms: Public domain | W3C validator |