![]() |
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 158 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | syld 45 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: 3imtr4d 203 sbciegft 2995 opeldmg 4834 elreldm 4855 ssimaex 5579 resflem 5682 f1eqcocnv 5794 fliftfun 5799 isopolem 5825 isosolem 5827 brtposg 6257 issmo2 6292 nnmcl 6484 nnawordi 6518 nnmordi 6519 nnmord 6520 swoord1 6566 ecopovtrn 6634 ecopovtrng 6637 f1domg 6760 mapen 6848 mapxpen 6850 supmoti 6994 isotilem 7007 exmidomniim 7141 enq0tr 7435 prubl 7487 ltexprlemloc 7608 addextpr 7622 recexprlem1ssl 7634 recexprlem1ssu 7635 cauappcvgprlemdisj 7652 mulcmpblnr 7742 mulgt0sr 7779 map2psrprg 7806 ltleletr 8041 ltle 8047 ltadd2 8378 leltadd 8406 reapti 8538 apreap 8546 reapcotr 8557 apcotr 8566 addext 8569 mulext1 8571 zapne 9329 zextle 9346 prime 9354 uzin 9562 indstr 9595 supinfneg 9597 infsupneg 9598 ublbneg 9615 xrltle 9800 xrre2 9823 icc0r 9928 fzrevral 10107 flqge 10284 modqadd1 10363 modqmul1 10379 facdiv 10720 resqrexlemgt0 11031 abs00ap 11073 absext 11074 climshftlemg 11312 climcaucn 11361 dvds2lem 11812 dvdsfac 11868 ltoddhalfle 11900 ndvdsadd 11938 gcdaddm 11987 bezoutlembi 12008 gcdzeq 12025 algcvga 12053 rpdvds 12101 cncongr1 12105 cncongr2 12106 prmind2 12122 euclemma 12148 isprm6 12149 rpexp 12155 sqrt2irr 12164 odzdvds 12247 pclemub 12289 pceulem 12296 pc2dvds 12331 fldivp1 12348 infpnlem1 12359 prmunb 12362 issubg4m 13058 fiinbas 13634 bastg 13646 tgcl 13649 opnssneib 13741 tgcnp 13794 iscnp4 13803 cnntr 13810 cnptopresti 13823 lmss 13831 lmtopcnp 13835 txdis 13862 xblss2ps 13989 xblss2 13990 blsscls2 14078 metequiv2 14081 bdxmet 14086 mulc1cncf 14161 cncfco 14163 sincosq2sgn 14333 sincosq3sgn 14334 sincosq4sgn 14335 lgsdir 14521 2sqlem8a 14554 2sqlem10 14557 triap 14862 |
Copyright terms: Public domain | W3C validator |