![]() |
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 935 bm1.1 2162 eqtr3 2197 elnelne1 2451 elnelne2 2452 morex 2921 reuss2 3415 reupick 3419 rabsneu 3664 opabss 4064 triun 4111 poirr 4303 wepo 4355 wetrep 4356 rexxfrd 4459 reg3exmidlemwe 4574 nnsuc 4611 fnfco 5385 fun11iun 5477 fnressn 5697 fvpr1g 5717 fvtp1g 5719 fvtp3g 5721 fvtp3 5724 f1mpt 5765 caovlem2d 6060 offval 6083 dfoprab3 6185 1stconst 6215 2ndconst 6216 poxp 6226 tfrlemisucaccv 6319 tfr1onlemsucaccv 6335 tfrcllemsucaccv 6348 fiintim 6921 addclpi 7304 addnidpig 7313 reapmul1 8529 nnnn0addcl 9182 un0addcl 9185 un0mulcl 9186 zltnle 9275 nn0ge0div 9316 uzind3 9342 uzind4 9564 ltsubrp 9664 ltaddrp 9665 xrlttr 9769 xrltso 9770 xltnegi 9809 xaddnemnf 9831 xaddnepnf 9832 xaddcom 9835 xnegdi 9842 xsubge0 9855 fzind2 10212 qltnle 10219 qbtwnxr 10231 exp3vallem 10494 expp1 10500 expnegap0 10501 expcllem 10504 mulexpzap 10533 expaddzap 10537 expmulzap 10539 hashunlem 10755 shftf 10810 sqrtdiv 11022 mulcn2 11291 summodclem2 11361 fsum3 11366 cvgratz 11511 prodmodclem2 11556 zproddc 11558 prodsnf 11571 dvdsflip 11827 dvdsfac 11836 lcmgcdlem 12047 rpexp1i 12124 hashdvds 12191 hashgcdlem 12208 phisum 12210 pcqcl 12276 pcid 12293 ssnnctlemct 12417 issubmd 12742 grpinvnzcl 12818 mulgneg 12877 mulgnn0z 12885 lmss 13379 xmetrtri 13509 blssioo 13678 divcnap 13688 dedekindicc 13744 dvidlemap 13793 dvrecap 13810 dveflem 13820 lgsval3 14052 lgsdir2 14067 2sqlem6 14089 bj-bdfindes 14323 bj-findes 14355 |
Copyright terms: Public domain | W3C validator |