![]() |
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 6814 suplocsrlempr 7808 geo2lim 11526 fprodge0 11647 fprodge1 11649 oddp1d2 11897 bezoutlema 12002 bezoutlemb 12003 pythagtriplem1 12267 exmidunben 12429 ismet 13883 isxmet 13884 coseq0negpitopi 14296 cosq34lt1 14310 cos02pilt1 14311 logdivlti 14341 lgseisenlem1 14489 m1lgs 14491 |
Copyright terms: Public domain | W3C validator |