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: 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: syl2anb 289 dcor 919 bm1.1 2124 eqtr3 2159 elnelne1 2412 elnelne2 2413 morex 2868 reuss2 3356 reupick 3360 rabsneu 3596 opabss 3992 triun 4039 poirr 4229 wepo 4281 wetrep 4282 rexxfrd 4384 reg3exmidlemwe 4493 nnsuc 4529 fnfco 5297 fun11iun 5388 fnressn 5606 fvpr1g 5626 fvtp1g 5628 fvtp3g 5630 fvtp3 5633 f1mpt 5672 caovlem2d 5963 offval 5989 dfoprab3 6089 1stconst 6118 2ndconst 6119 poxp 6129 tfrlemisucaccv 6222 tfr1onlemsucaccv 6238 tfrcllemsucaccv 6251 fiintim 6817 addclpi 7135 addnidpig 7144 reapmul1 8357 nnnn0addcl 9007 un0addcl 9010 un0mulcl 9011 zltnle 9100 nn0ge0div 9138 uzind3 9164 uzind4 9383 ltsubrp 9478 ltaddrp 9479 xrlttr 9581 xrltso 9582 xltnegi 9618 xaddnemnf 9640 xaddnepnf 9641 xaddcom 9644 xnegdi 9651 xsubge0 9664 fzind2 10016 qltnle 10023 qbtwnxr 10035 exp3vallem 10294 expp1 10300 expnegap0 10301 expcllem 10304 mulexpzap 10333 expaddzap 10337 expmulzap 10339 hashunlem 10550 shftf 10602 sqrtdiv 10814 mulcn2 11081 summodclem2 11151 fsum3 11156 cvgratz 11301 prodmodclem2 11346 dvdsflip 11549 dvdsfac 11558 lcmgcdlem 11758 rpexp1i 11832 hashdvds 11897 hashgcdlem 11903 lmss 12415 xmetrtri 12545 blssioo 12714 divcnap 12724 dedekindicc 12780 dvidlemap 12829 dvrecap 12846 dveflem 12855 bj-bdfindes 13147 bj-findes 13179 |
Copyright terms: Public domain | W3C validator |