![]() |
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 158 | . 2 ⊢ (𝜑 → (𝜒 → 𝜃)) |
4 | 1, 3 | syld 45 | 1 ⊢ (𝜑 → (𝜓 → 𝜃)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 105 |
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 3008 opeldmg 4850 elreldm 4871 ssimaex 5598 resflem 5701 f1eqcocnv 5813 fliftfun 5818 isopolem 5844 isosolem 5846 brtposg 6279 issmo2 6314 nnmcl 6506 nnawordi 6540 nnmordi 6541 nnmord 6542 swoord1 6588 ecopovtrn 6658 ecopovtrng 6661 f1domg 6784 mapen 6874 mapxpen 6876 supmoti 7022 isotilem 7035 exmidomniim 7169 enq0tr 7463 prubl 7515 ltexprlemloc 7636 addextpr 7650 recexprlem1ssl 7662 recexprlem1ssu 7663 cauappcvgprlemdisj 7680 mulcmpblnr 7770 mulgt0sr 7807 map2psrprg 7834 ltleletr 8069 ltle 8075 ltadd2 8406 leltadd 8434 reapti 8566 apreap 8574 reapcotr 8585 apcotr 8594 addext 8597 mulext1 8599 zapne 9357 zextle 9374 prime 9382 uzin 9590 indstr 9623 supinfneg 9625 infsupneg 9626 ublbneg 9643 xrltle 9828 xrre2 9851 icc0r 9956 fzrevral 10135 flqge 10313 modqadd1 10392 modqmul1 10408 facdiv 10750 resqrexlemgt0 11061 abs00ap 11103 absext 11104 climshftlemg 11342 climcaucn 11391 dvds2lem 11842 dvdsfac 11898 ltoddhalfle 11930 ndvdsadd 11968 gcdaddm 12017 bezoutlembi 12038 gcdzeq 12055 algcvga 12083 rpdvds 12131 cncongr1 12135 cncongr2 12136 prmind2 12152 euclemma 12178 isprm6 12179 rpexp 12185 sqrt2irr 12194 odzdvds 12277 pclemub 12319 pceulem 12326 pc2dvds 12362 fldivp1 12380 infpnlem1 12391 prmunb 12394 issubg4m 13132 imasabl 13273 fiinbas 14006 bastg 14018 tgcl 14021 opnssneib 14113 tgcnp 14166 iscnp4 14175 cnntr 14182 cnptopresti 14195 lmss 14203 lmtopcnp 14207 txdis 14234 xblss2ps 14361 xblss2 14362 blsscls2 14450 metequiv2 14453 bdxmet 14458 mulc1cncf 14533 cncfco 14535 sincosq2sgn 14705 sincosq3sgn 14706 sincosq4sgn 14707 lgsdir 14894 2sqlem8a 14927 2sqlem10 14930 triap 15236 |
Copyright terms: Public domain | W3C validator |