![]() |
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: ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 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 2870 opeldmg 4654 elreldm 4674 ssimaex 5378 resflem 5476 f1eqcocnv 5584 fliftfun 5589 isopolem 5615 isosolem 5617 brtposg 6033 issmo2 6068 nnmcl 6256 nnawordi 6288 nnmordi 6289 nnmord 6290 swoord1 6335 ecopovtrn 6403 ecopovtrng 6406 f1domg 6529 mapen 6616 mapxpen 6618 supmoti 6742 isotilem 6755 exmidomniim 6858 enq0tr 7054 prubl 7106 ltexprlemloc 7227 addextpr 7241 recexprlem1ssl 7253 recexprlem1ssu 7254 cauappcvgprlemdisj 7271 mulcmpblnr 7348 mulgt0sr 7384 ltleletr 7628 ltle 7633 ltadd2 7958 leltadd 7986 reapti 8117 apreap 8125 reapcotr 8136 apcotr 8145 addext 8148 mulext1 8150 zapne 8882 zextle 8898 prime 8906 uzin 9112 indstr 9142 supinfneg 9144 infsupneg 9145 ublbneg 9159 xrltle 9329 xrre2 9344 icc0r 9405 fzrevral 9580 flqge 9750 modqadd1 9829 modqmul1 9845 facdiv 10207 resqrexlemgt0 10514 abs00ap 10556 absext 10557 climshftlemg 10751 climcaucn 10801 dvds2lem 11147 dvdsfac 11200 ltoddhalfle 11232 ndvdsadd 11270 gcdaddm 11314 bezoutlembi 11333 gcdzeq 11350 algcvga 11372 rpdvds 11420 cncongr1 11424 cncongr2 11425 prmind2 11441 euclemma 11464 isprm6 11465 rpexp 11471 sqrt2irr 11480 fiinbas 11808 bastg 11822 tgcl 11825 mulc1cncf 11918 cncfco 11920 |
Copyright terms: Public domain | W3C validator |