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 904 bm1.1 2102 eqtr3 2137 elnelne1 2389 elnelne2 2390 morex 2841 reuss2 3326 reupick 3330 rabsneu 3566 opabss 3962 triun 4009 poirr 4199 wepo 4251 wetrep 4252 rexxfrd 4354 reg3exmidlemwe 4463 nnsuc 4499 fnfco 5267 fun11iun 5356 fnressn 5574 fvpr1g 5594 fvtp1g 5596 fvtp3g 5598 fvtp3 5601 f1mpt 5640 caovlem2d 5931 offval 5957 dfoprab3 6057 1stconst 6086 2ndconst 6087 poxp 6097 tfrlemisucaccv 6190 tfr1onlemsucaccv 6206 tfrcllemsucaccv 6219 fiintim 6785 addclpi 7103 addnidpig 7112 reapmul1 8325 nnnn0addcl 8975 un0addcl 8978 un0mulcl 8979 zltnle 9068 nn0ge0div 9106 uzind3 9132 uzind4 9351 ltsubrp 9446 ltaddrp 9447 xrlttr 9549 xrltso 9550 xltnegi 9586 xaddnemnf 9608 xaddnepnf 9609 xaddcom 9612 xnegdi 9619 xsubge0 9632 fzind2 9984 qltnle 9991 qbtwnxr 10003 exp3vallem 10262 expp1 10268 expnegap0 10269 expcllem 10272 mulexpzap 10301 expaddzap 10305 expmulzap 10307 hashunlem 10518 shftf 10570 sqrtdiv 10782 mulcn2 11049 summodclem2 11119 fsum3 11124 cvgratz 11269 dvdsflip 11476 dvdsfac 11485 lcmgcdlem 11685 rpexp1i 11759 hashdvds 11824 hashgcdlem 11830 lmss 12342 xmetrtri 12472 blssioo 12641 divcnap 12651 dedekindicc 12707 dvidlemap 12756 dvrecap 12773 dveflem 12782 bj-bdfindes 13074 bj-findes 13106 |
Copyright terms: Public domain | W3C validator |