New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > 3syl | GIF version |
Description: Inference chaining two syllogisms. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
3syl.1 | ⊢ (φ → ψ) |
3syl.2 | ⊢ (ψ → χ) |
3syl.3 | ⊢ (χ → θ) |
Ref | Expression |
---|---|
3syl | ⊢ (φ → θ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3syl.1 | . . 3 ⊢ (φ → ψ) | |
2 | 3syl.2 | . . 3 ⊢ (ψ → χ) | |
3 | 1, 2 | syl 15 | . 2 ⊢ (φ → χ) |
4 | 3syl.3 | . 2 ⊢ (χ → θ) | |
5 | 3, 4 | syl 15 | 1 ⊢ (φ → θ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 |
This theorem is referenced by: nic-ax 1438 merco2 1501 alcomiw 1704 hbn1fw 1705 hba1w 1707 ax5o 1749 hba1OLD 1787 ax16i 2046 hba1-o 2149 ax67to6 2167 ax467 2169 ax467to6 2171 aev-o 2182 ax10-16 2190 mo 2226 eupickb 2269 2eu2 2285 2reu5 3044 sbcco3g 3191 imakexg 4299 intexg 4319 addcexg 4393 nnsucelr 4428 ncfineleq 4477 oddnn 4507 evenodddisj 4516 sfintfin 4532 imaexg 4746 coexg 4749 siexg 4752 fnresdm 5192 foima 5274 f1imacnv 5302 f1osng 5323 oprabid 5550 imageexg 5800 fullfunexg 5859 erth 5968 qsexg 5982 pmex 6005 map0 6025 enpw1 6062 enprmaplem3 6078 enprmaplem6 6081 ncdisjun 6136 ovcelem1 6171 lenc 6223 nchoicelem8 6296 nchoicelem14 6302 nchoicelem17 6305 dmfrec 6316 fnfreclem1 6317 fnfrec 6320 |
Copyright terms: Public domain | W3C validator |