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 1969 ceqsalt 2686 sbceqal 2936 csbiebt 3009 rspcsbela 3029 preqr1g 3663 repizf2 4056 copsexg 4136 onun2 4376 suc11g 4442 elrnrexdm 5527 isoselem 5689 riotass2 5724 oawordriexmid 6334 nnm00 6393 ecopovtrn 6494 ecopovtrng 6497 infglbti 6880 difinfsnlem 6952 enq0tr 7210 addnqprl 7305 addnqpru 7306 mulnqprl 7344 mulnqpru 7345 recexprlemss1l 7411 recexprlemss1u 7412 cauappcvgprlemdisj 7427 mulextsr1lem 7556 pitonn 7624 rereceu 7665 cnegexlem1 7905 ltadd2 8149 eqord2 8214 mulext 8344 mulgt1 8589 lt2halves 8923 addltmul 8924 nzadd 9074 zextlt 9111 recnz 9112 zeo 9124 peano5uzti 9127 irradd 9406 irrmul 9407 xltneg 9587 xleadd1 9626 icc0r 9677 fznuz 9850 uznfz 9851 facndiv 10453 rennim 10742 abs00ap 10802 absle 10829 cau3lem 10854 caubnd2 10857 climshft 11041 subcn2 11048 mulcn2 11049 serf0 11089 cvgratnnlemnexp 11261 cvgratnnlemmn 11262 efieq1re 11405 moddvds 11429 dvdsssfz1 11477 nn0seqcvgd 11649 algcvgblem 11657 eucalglt 11665 lcmgcdlem 11685 rpmul 11706 divgcdcoprm0 11709 isprm6 11752 rpexp 11758 tgss3 12174 cnpnei 12315 cnntr 12321 hmeoopn 12407 hmeocld 12408 mulcncflem 12686 sincosq3sgn 12836 sincosq4sgn 12837 bj-peano4 13080 |
Copyright terms: Public domain | W3C validator |