Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mp3an12i | Unicode version |
Description: mp3an 1326 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 1316 | . 2 |
6 | 1, 5 | syl 14 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 w3a 967 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 969 |
This theorem is referenced by: map1 6769 suplocsrlempr 7739 geo2lim 11443 fprodge0 11564 fprodge1 11566 oddp1d2 11812 bezoutlema 11917 bezoutlemb 11918 pythagtriplem1 12174 exmidunben 12296 ismet 12885 isxmet 12886 coseq0negpitopi 13298 cosq34lt1 13312 cos02pilt1 13313 logdivlti 13343 |
Copyright terms: Public domain | W3C validator |