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 143 | . 2 |
4 | 1, 3 | syld 45 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: 3imtr3d 201 dvelimdf 2003 ceqsalt 2747 sbceqal 3001 csbiebt 3079 rspcsbela 3099 preqr1g 3740 repizf2 4135 copsexg 4216 onun2 4461 suc11g 4528 elrnrexdm 5618 isoselem 5782 riotass2 5818 oawordriexmid 6429 nnm00 6488 ecopovtrn 6589 ecopovtrng 6592 infglbti 6981 difinfsnlem 7055 enq0tr 7366 addnqprl 7461 addnqpru 7462 mulnqprl 7500 mulnqpru 7501 recexprlemss1l 7567 recexprlemss1u 7568 cauappcvgprlemdisj 7583 mulextsr1lem 7712 pitonn 7780 rereceu 7821 cnegexlem1 8064 ltadd2 8308 eqord2 8373 mulext 8503 mulgt1 8749 lt2halves 9083 addltmul 9084 nzadd 9234 ltsubnn0 9249 zextlt 9274 recnz 9275 zeo 9287 peano5uzti 9290 irradd 9575 irrmul 9576 xltneg 9763 xleadd1 9802 icc0r 9853 fznuz 10027 uznfz 10028 facndiv 10641 rennim 10930 abs00ap 10990 absle 11017 cau3lem 11042 caubnd2 11045 climshft 11231 subcn2 11238 mulcn2 11239 serf0 11279 cvgratnnlemnexp 11451 cvgratnnlemmn 11452 efieq1re 11698 moddvds 11725 dvdsssfz1 11775 nn0seqcvgd 11952 algcvgblem 11960 eucalglt 11968 lcmgcdlem 11988 rpmul 12009 divgcdcoprm0 12012 isprm6 12058 rpexp 12064 eulerthlema 12141 eulerthlemh 12142 prmdiv 12146 pcprendvds2 12202 pcz 12242 pcprmpw 12244 pcfac 12259 expnprm 12262 tgss3 12625 cnpnei 12766 cnntr 12772 hmeoopn 12858 hmeocld 12859 mulcncflem 13137 sincosq3sgn 13296 sincosq4sgn 13297 bj-peano4 13678 iswomni0 13771 |
Copyright terms: Public domain | W3C validator |