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 2750 reusv1 4418 fliftcnv 5745 fliftfun 5746 tfrlemibfn 6275 tfr1onlembfn 6291 tfrcllembfn 6304 cnvct 6754 ordiso 6980 exmidomni 7085 djudoml 7154 djudomr 7155 uzsinds 10341 fimaxq 10701 ltoddhalfle 11783 phicl2 12088 strsetsid 12223 txdis1cn 12678 xmeter 12836 subctctexmid 13573 |
Copyright terms: Public domain | W3C validator |