New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > sylbid | GIF version |
Description: A syllogism deduction. (Contributed by NM, 3-Aug-1994.) |
Ref | Expression |
---|---|
sylbid.1 | ⊢ (φ → (ψ ↔ χ)) |
sylbid.2 | ⊢ (φ → (χ → θ)) |
Ref | Expression |
---|---|
sylbid | ⊢ (φ → (ψ → θ)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylbid.1 | . . 3 ⊢ (φ → (ψ ↔ χ)) | |
2 | 1 | biimpd 198 | . 2 ⊢ (φ → (ψ → χ)) |
3 | sylbid.2 | . 2 ⊢ (φ → (χ → θ)) | |
4 | 2, 3 | syld 40 | 1 ⊢ (φ → (ψ → θ)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 176 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 |
This theorem depends on definitions: df-bi 177 |
This theorem is referenced by: 3imtr4d 259 ax11eq 2193 ax11el 2194 leltfintr 4458 tfin11 4493 sfinltfin 4535 phi11lem1 4595 xp11 5056 xpcan 5057 xpcan2 5058 enprmaplem3 6078 enprmaplem6 6081 ce0addcnnul 6179 ceclb 6183 fce 6188 sbth 6206 dflec2 6210 lectr 6211 leaddc1 6214 leconnnc 6218 tlecg 6229 letc 6230 ce0lenc1 6238 nclenn 6248 lemuc1 6252 lecadd2 6265 ncslesuc 6266 nchoicelem9 6295 nchoicelem12 6298 nchoicelem17 6303 dmfrec 6314 fnfreclem2 6316 fnfreclem3 6317 |
Copyright terms: Public domain | W3C validator |