![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > sylibd | GIF version |
Description: A syllogism deduction. (Contributed by NM, 3-Aug-1994.) |
Ref | Expression |
---|---|
sylibd.1 | ⊢ (φ → (ψ → χ)) |
sylibd.2 | ⊢ (φ → (χ ↔ θ)) |
Ref | Expression |
---|---|
sylibd | ⊢ (φ → (ψ → θ)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylibd.1 | . 2 ⊢ (φ → (ψ → χ)) | |
2 | sylibd.2 | . . 3 ⊢ (φ → (χ ↔ θ)) | |
3 | 2 | biimpd 132 | . 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 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: 3imtr3d 191 dvelimdf 1889 ceqsalt 2574 sbceqal 2808 sbcimdv 2817 csbiebt 2880 rspcsbela 2899 preqr1g 3528 repizf2 3906 copsexg 3972 onun2 4182 suc11g 4235 elrnrexdm 5249 isoselem 5402 riotass2 5437 nnm00 6038 ecopovtrn 6139 ecopovtrng 6142 enq0tr 6417 addnqprl 6512 addnqpru 6513 mulnqprl 6549 mulnqpru 6550 recexprlemss1l 6607 recexprlemss1u 6608 cauappcvgprlemdisj 6623 mulextsr1lem 6706 pitonn 6744 cnegexlem1 6983 ltadd2 7212 mulext 7398 mulgt1 7610 lt2halves 7937 addltmul 7938 zextlt 8108 recnz 8109 zeo 8119 peano5uzti 8122 irradd 8355 irrmul 8356 xltneg 8519 icc0r 8565 fznuz 8734 uznfz 8735 rennim 9211 bj-peano4 9415 |
Copyright terms: Public domain | W3C validator |