![]() |
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 2775 reusv1 4458 fliftcnv 5795 fliftfun 5796 tfrlemibfn 6328 tfr1onlembfn 6344 tfrcllembfn 6357 cnvct 6808 ordiso 7034 exmidomni 7139 djudoml 7217 djudomr 7218 uzsinds 10439 fimaxq 10802 ltoddhalfle 11892 phicl2 12208 strsetsid 12489 txdis1cn 13671 xmeter 13829 subctctexmid 14632 |
Copyright terms: Public domain | W3C validator |