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 147 | . 2 ⊢ (𝜑 → (𝜒 → 𝜃)) |
4 | 1, 3 | syld 40 | 1 ⊢ (𝜑 → (𝜓 → 𝜃)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 98 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: 3imtr4d 192 sbciegft 2793 eqsbc3r 2819 opeldmg 4540 elreldm 4560 ssimaex 5234 f1eqcocnv 5431 fliftfun 5436 isopolem 5461 isosolem 5463 brtposg 5869 issmo2 5904 rdgon 5973 frecsuclem3 5990 freccl 5993 nnmcl 6060 nnawordi 6088 nnmordi 6089 nnmord 6090 swoord1 6135 ecopovtrn 6203 ecopovtrng 6206 f1domg 6238 enq0tr 6532 prubl 6584 ltexprlemloc 6705 addextpr 6719 recexprlem1ssl 6731 recexprlem1ssu 6732 cauappcvgprlemdisj 6749 mulcmpblnr 6826 mulgt0sr 6862 ltleletr 7100 ltle 7105 ltadd2 7416 leltadd 7442 reapti 7570 apreap 7578 reapcotr 7589 apcotr 7598 addext 7601 mulext1 7603 zapne 8315 zextle 8331 prime 8337 uzin 8505 indstr 8536 ublbneg 8548 xrltle 8719 xrre2 8734 icc0r 8795 fzrevral 8967 flqge 9124 resqrexlemgt0 9618 abs00ap 9660 absext 9661 climshftlemg 9823 climcaucn 9870 sqrt2irr 9878 ialgcvga 9890 |
Copyright terms: Public domain | W3C validator |