![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mpisyl | GIF version |
Description: A syllogism combined with a modus ponens inference. (Contributed by Alan Sare, 25-Jul-2011.) |
Ref | Expression |
---|---|
mpisyl.1 | ⊢ (𝜑 → 𝜓) |
mpisyl.2 | ⊢ 𝜒 |
mpisyl.3 | ⊢ (𝜓 → (𝜒 → 𝜃)) |
Ref | Expression |
---|---|
mpisyl | ⊢ (𝜑 → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpisyl.1 | . 2 ⊢ (𝜑 → 𝜓) | |
2 | mpisyl.2 | . . 3 ⊢ 𝜒 | |
3 | mpisyl.3 | . . 3 ⊢ (𝜓 → (𝜒 → 𝜃)) | |
4 | 2, 3 | mpi 15 | . 2 ⊢ (𝜓 → 𝜃) |
5 | 1, 4 | syl 14 | 1 ⊢ (𝜑 → 𝜃) |
Colors of variables: wff set 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: ceqsex 2727 reusv1 4387 fliftcnv 5704 fliftfun 5705 tfrlemibfn 6233 tfr1onlembfn 6249 tfrcllembfn 6262 cnvct 6711 ordiso 6929 exmidomni 7022 djudoml 7092 djudomr 7093 uzsinds 10246 fimaxq 10605 ltoddhalfle 11626 phicl2 11926 strsetsid 12031 txdis1cn 12486 xmeter 12644 subctctexmid 13369 |
Copyright terms: Public domain | W3C validator |