![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mp3an12i | Unicode 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: ![]() ![]() |
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 6806 suplocsrlempr 7794 geo2lim 11505 fprodge0 11626 fprodge1 11628 oddp1d2 11875 bezoutlema 11980 bezoutlemb 11981 pythagtriplem1 12245 exmidunben 12407 ismet 13504 isxmet 13505 coseq0negpitopi 13917 cosq34lt1 13931 cos02pilt1 13932 logdivlti 13962 |
Copyright terms: Public domain | W3C validator |