Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > sylibrd | GIF 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 2985 opeldmg 4816 elreldm 4837 ssimaex 5557 resflem 5660 f1eqcocnv 5770 fliftfun 5775 isopolem 5801 isosolem 5803 brtposg 6233 issmo2 6268 nnmcl 6460 nnawordi 6494 nnmordi 6495 nnmord 6496 swoord1 6542 ecopovtrn 6610 ecopovtrng 6613 f1domg 6736 mapen 6824 mapxpen 6826 supmoti 6970 isotilem 6983 exmidomniim 7117 enq0tr 7396 prubl 7448 ltexprlemloc 7569 addextpr 7583 recexprlem1ssl 7595 recexprlem1ssu 7596 cauappcvgprlemdisj 7613 mulcmpblnr 7703 mulgt0sr 7740 map2psrprg 7767 ltleletr 8001 ltle 8007 ltadd2 8338 leltadd 8366 reapti 8498 apreap 8506 reapcotr 8517 apcotr 8526 addext 8529 mulext1 8531 zapne 9286 zextle 9303 prime 9311 uzin 9519 indstr 9552 supinfneg 9554 infsupneg 9555 ublbneg 9572 xrltle 9755 xrre2 9778 icc0r 9883 fzrevral 10061 flqge 10238 modqadd1 10317 modqmul1 10333 facdiv 10672 resqrexlemgt0 10984 abs00ap 11026 absext 11027 climshftlemg 11265 climcaucn 11314 dvds2lem 11765 dvdsfac 11820 ltoddhalfle 11852 ndvdsadd 11890 gcdaddm 11939 bezoutlembi 11960 gcdzeq 11977 algcvga 12005 rpdvds 12053 cncongr1 12057 cncongr2 12058 prmind2 12074 euclemma 12100 isprm6 12101 rpexp 12107 sqrt2irr 12116 odzdvds 12199 pclemub 12241 pceulem 12248 pc2dvds 12283 fldivp1 12300 infpnlem1 12311 prmunb 12314 fiinbas 12841 bastg 12855 tgcl 12858 opnssneib 12950 tgcnp 13003 iscnp4 13012 cnntr 13019 cnptopresti 13032 lmss 13040 lmtopcnp 13044 txdis 13071 xblss2ps 13198 xblss2 13199 blsscls2 13287 metequiv2 13290 bdxmet 13295 mulc1cncf 13370 cncfco 13372 sincosq2sgn 13542 sincosq3sgn 13543 sincosq4sgn 13544 lgsdir 13730 2sqlem8a 13752 2sqlem10 13755 triap 14061 |
Copyright terms: Public domain | W3C validator |