New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > sylancr | GIF version |
Description: Syllogism inference combined with modus ponens. (Contributed by Jeff Madsen, 2-Sep-2009.) |
Ref | Expression |
---|---|
sylancr.1 | ⊢ ψ |
sylancr.2 | ⊢ (φ → χ) |
sylancr.3 | ⊢ ((ψ ∧ χ) → θ) |
Ref | Expression |
---|---|
sylancr | ⊢ (φ → θ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylancr.1 | . . 3 ⊢ ψ | |
2 | 1 | a1i 10 | . 2 ⊢ (φ → ψ) |
3 | sylancr.2 | . 2 ⊢ (φ → χ) | |
4 | sylancr.3 | . 2 ⊢ ((ψ ∧ χ) → θ) | |
5 | 2, 3, 4 | syl2anc 642 | 1 ⊢ (φ → θ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 358 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 177 df-an 360 |
This theorem is referenced by: unipw 4117 imakexg 4299 pwexg 4328 snfi 4431 1cspfin 4543 vfintle 4546 vfin1cltv 4547 phialllem2 4617 coexg 4749 ov 5595 mpteq2da 5666 brcupg 5814 brcomposeg 5819 brcrossg 5848 frds 5935 qsexg 5982 enmap2lem5 6067 enmap1lem5 6073 enprmaplem6 6081 enpw 6087 dflec2 6210 nmembers1lem3 6270 nchoicelem19 6307 frecexg 6312 dmfrec 6316 fnfreclem1 6317 fnfreclem2 6318 fnfreclem3 6319 frec0 6321 frecsuc 6322 |
Copyright terms: Public domain | W3C validator |