![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mp3an12i | GIF version |
Description: mp3an 1348 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 1338 | . 2 ⊢ (𝜃 → 𝜏) |
6 | 1, 5 | syl 14 | 1 ⊢ (𝜒 → 𝜏) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 980 |
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 982 |
This theorem is referenced by: map1 6866 exmidpw2en 6968 suplocsrlempr 7867 geo2lim 11659 fprodge0 11780 fprodge1 11782 oddp1d2 12031 bezoutlema 12136 bezoutlemb 12137 pythagtriplem1 12403 exmidunben 12583 psrelbas 14160 psraddcl 14164 ismet 14512 isxmet 14513 coseq0negpitopi 14971 cosq34lt1 14985 cos02pilt1 14986 logdivlti 15016 lgseisenlem1 15186 lgseisen 15190 m1lgs 15192 |
Copyright terms: Public domain | W3C validator |