Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > sylibd | Unicode version |
Description: A syllogism deduction. (Contributed by NM, 3-Aug-1994.) |
Ref | Expression |
---|---|
sylibd.1 | |
sylibd.2 |
Ref | Expression |
---|---|
sylibd |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylibd.1 | . 2 | |
2 | sylibd.2 | . . 3 | |
3 | 2 | biimpd 132 | . 2 |
4 | 1, 3 | syld 40 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 98 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: 3imtr3d 191 dvelimdf 1892 ceqsalt 2580 sbceqal 2814 sbcimdv 2823 csbiebt 2886 rspcsbela 2905 preqr1g 3537 repizf2 3915 copsexg 3981 onun2 4216 suc11g 4281 elrnrexdm 5306 isoselem 5459 riotass2 5494 nnm00 6102 ecopovtrn 6203 ecopovtrng 6206 enq0tr 6532 addnqprl 6627 addnqpru 6628 mulnqprl 6666 mulnqpru 6667 recexprlemss1l 6733 recexprlemss1u 6734 cauappcvgprlemdisj 6749 mulextsr1lem 6864 pitonn 6924 rereceu 6963 cnegexlem1 7186 ltadd2 7416 mulext 7605 mulgt1 7829 lt2halves 8160 addltmul 8161 zextlt 8332 recnz 8333 zeo 8343 peano5uzti 8346 irradd 8580 irrmul 8581 xltneg 8749 icc0r 8795 fznuz 8964 uznfz 8965 rennim 9600 abs00ap 9660 absle 9685 cau3lem 9710 caubnd2 9713 climshft 9825 subcn2 9832 mulcn2 9833 serif0 9871 nn0seqcvgd 9880 algcvgblem 9888 bj-peano4 10080 |
Copyright terms: Public domain | W3C validator |