![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mp3an12i | GIF version |
Description: mp3an 1337 with antecedents in standard conjunction form and with one hypothesis an implication. (Contributed by Alan Sare, 28-Aug-2016.) |
Ref | Expression |
---|---|
mp3an12i.1 | ⊢ 𝜑 |
mp3an12i.2 | ⊢ 𝜓 |
mp3an12i.3 | ⊢ (𝜒 → 𝜃) |
mp3an12i.4 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏) |
Ref | Expression |
---|---|
mp3an12i | ⊢ (𝜒 → 𝜏) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mp3an12i.3 | . 2 ⊢ (𝜒 → 𝜃) | |
2 | mp3an12i.1 | . . 3 ⊢ 𝜑 | |
3 | mp3an12i.2 | . . 3 ⊢ 𝜓 | |
4 | mp3an12i.4 | . . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏) | |
5 | 2, 3, 4 | mp3an12 1327 | . 2 ⊢ (𝜃 → 𝜏) |
6 | 1, 5 | syl 14 | 1 ⊢ (𝜒 → 𝜏) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 978 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 df-3an 980 |
This theorem is referenced by: map1 6811 suplocsrlempr 7805 geo2lim 11519 fprodge0 11640 fprodge1 11642 oddp1d2 11889 bezoutlema 11994 bezoutlemb 11995 pythagtriplem1 12259 exmidunben 12421 ismet 13775 isxmet 13776 coseq0negpitopi 14188 cosq34lt1 14202 cos02pilt1 14203 logdivlti 14233 |
Copyright terms: Public domain | W3C validator |