Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > sylibrd | Unicode version |
Description: A syllogism deduction. (Contributed by NM, 3-Aug-1994.) |
Ref | Expression |
---|---|
sylibrd.1 | |
sylibrd.2 |
Ref | Expression |
---|---|
sylibrd |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylibrd.1 | . 2 | |
2 | sylibrd.2 | . . 3 | |
3 | 2 | biimprd 157 | . 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 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: 3imtr4d 202 sbciegft 2911 opeldmg 4714 elreldm 4735 ssimaex 5450 resflem 5552 f1eqcocnv 5660 fliftfun 5665 isopolem 5691 isosolem 5693 brtposg 6119 issmo2 6154 nnmcl 6345 nnawordi 6379 nnmordi 6380 nnmord 6381 swoord1 6426 ecopovtrn 6494 ecopovtrng 6497 f1domg 6620 mapen 6708 mapxpen 6710 supmoti 6848 isotilem 6861 exmidomniim 6981 enq0tr 7210 prubl 7262 ltexprlemloc 7383 addextpr 7397 recexprlem1ssl 7409 recexprlem1ssu 7410 cauappcvgprlemdisj 7427 mulcmpblnr 7517 mulgt0sr 7554 map2psrprg 7581 ltleletr 7814 ltle 7819 ltadd2 8149 leltadd 8177 reapti 8309 apreap 8317 reapcotr 8328 apcotr 8337 addext 8340 mulext1 8342 cnstab 8375 zapne 9093 zextle 9110 prime 9118 uzin 9326 indstr 9356 supinfneg 9358 infsupneg 9359 ublbneg 9373 xrltle 9552 xrre2 9572 icc0r 9677 fzrevral 9853 flqge 10023 modqadd1 10102 modqmul1 10118 facdiv 10452 resqrexlemgt0 10760 abs00ap 10802 absext 10803 climshftlemg 11039 climcaucn 11088 dvds2lem 11432 dvdsfac 11485 ltoddhalfle 11517 ndvdsadd 11555 gcdaddm 11599 bezoutlembi 11620 gcdzeq 11637 algcvga 11659 rpdvds 11707 cncongr1 11711 cncongr2 11712 prmind2 11728 euclemma 11751 isprm6 11752 rpexp 11758 sqrt2irr 11767 fiinbas 12143 bastg 12157 tgcl 12160 opnssneib 12252 tgcnp 12305 iscnp4 12314 cnntr 12321 cnptopresti 12334 lmss 12342 lmtopcnp 12346 txdis 12373 xblss2ps 12500 xblss2 12501 blsscls2 12589 metequiv2 12592 bdxmet 12597 mulc1cncf 12672 cncfco 12674 sincosq2sgn 12835 sincosq3sgn 12836 sincosq4sgn 12837 triap 13151 |
Copyright terms: Public domain | W3C validator |