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 156 | . 2 ⊢ (𝜑 → (𝜒 → 𝜃)) |
4 | 1, 3 | syld 44 | 1 ⊢ (𝜑 → (𝜓 → 𝜃)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 103 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: 3imtr4d 201 sbciegft 2844 opeldmg 4558 elreldm 4578 ssimaex 5255 f1eqcocnv 5451 fliftfun 5456 isopolem 5481 isosolem 5483 brtposg 5892 issmo2 5927 rdgon 5996 frecsuclem3 6013 freccl 6016 nnmcl 6083 nnawordi 6111 nnmordi 6112 nnmord 6113 swoord1 6158 ecopovtrn 6226 ecopovtrng 6229 f1domg 6261 supmoti 6406 isotilem 6419 enq0tr 6624 prubl 6676 ltexprlemloc 6797 addextpr 6811 recexprlem1ssl 6823 recexprlem1ssu 6824 cauappcvgprlemdisj 6841 mulcmpblnr 6918 mulgt0sr 6954 ltleletr 7193 ltle 7198 ltadd2 7523 leltadd 7551 reapti 7679 apreap 7687 reapcotr 7698 apcotr 7707 addext 7710 mulext1 7712 zapne 8422 zextle 8438 prime 8446 uzin 8651 indstr 8681 supinfneg 8683 infsupneg 8684 ublbneg 8698 xrltle 8873 xrre2 8888 icc0r 8949 fzrevral 9122 flqge 9284 modqadd1 9363 modqmul1 9379 facdiv 9665 resqrexlemgt0 9906 abs00ap 9948 absext 9949 climshftlemg 10141 climcaucn 10188 dvds2lem 10207 dvdsfac 10260 ltoddhalfle 10293 ndvdsadd 10331 gcdaddm 10375 bezoutlembi 10394 gcdzeq 10411 ialgcvga 10433 rpdvds 10481 cncongr1 10485 cncongr2 10486 prmind2 10502 euclemma 10525 isprm6 10526 rpexp 10532 sqrt2irr 10541 |
Copyright terms: Public domain | W3C validator |