![]() |
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-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 2905 opeldmg 4702 elreldm 4723 ssimaex 5434 resflem 5536 f1eqcocnv 5644 fliftfun 5649 isopolem 5675 isosolem 5677 brtposg 6103 issmo2 6138 nnmcl 6329 nnawordi 6363 nnmordi 6364 nnmord 6365 swoord1 6410 ecopovtrn 6478 ecopovtrng 6481 f1domg 6604 mapen 6691 mapxpen 6693 supmoti 6830 isotilem 6843 exmidomniim 6961 enq0tr 7184 prubl 7236 ltexprlemloc 7357 addextpr 7371 recexprlem1ssl 7383 recexprlem1ssu 7384 cauappcvgprlemdisj 7401 mulcmpblnr 7478 mulgt0sr 7514 ltleletr 7763 ltle 7768 ltadd2 8094 leltadd 8122 reapti 8253 apreap 8261 reapcotr 8272 apcotr 8281 addext 8284 mulext1 8286 cnstab 8318 zapne 9023 zextle 9040 prime 9048 uzin 9254 indstr 9284 supinfneg 9286 infsupneg 9287 ublbneg 9301 xrltle 9471 xrre2 9491 icc0r 9596 fzrevral 9772 flqge 9942 modqadd1 10021 modqmul1 10037 facdiv 10371 resqrexlemgt0 10678 abs00ap 10720 absext 10721 climshftlemg 10957 climcaucn 11006 dvds2lem 11347 dvdsfac 11400 ltoddhalfle 11432 ndvdsadd 11470 gcdaddm 11514 bezoutlembi 11533 gcdzeq 11550 algcvga 11572 rpdvds 11620 cncongr1 11624 cncongr2 11625 prmind2 11641 euclemma 11664 isprm6 11665 rpexp 11671 sqrt2irr 11680 fiinbas 12053 bastg 12067 tgcl 12070 opnssneib 12162 tgcnp 12214 iscnp4 12223 cnntr 12230 cnptopresti 12243 lmss 12251 lmtopcnp 12255 txdis 12282 xblss2ps 12387 xblss2 12388 blsscls2 12476 metequiv2 12479 bdxmet 12484 mulc1cncf 12556 cncfco 12558 triap 12905 |
Copyright terms: Public domain | W3C validator |