![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mp3an2i | Unicode version |
Description: mp3an 1274 with antecedents in standard conjunction form and with two hypotheses which are implications. (Contributed by Alan Sare, 28-Aug-2016.) |
Ref | Expression |
---|---|
mp3an2i.1 |
![]() ![]() |
mp3an2i.2 |
![]() ![]() ![]() ![]() ![]() ![]() |
mp3an2i.3 |
![]() ![]() ![]() ![]() ![]() ![]() |
mp3an2i.4 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
mp3an2i |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mp3an2i.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | mp3an2i.3 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | mp3an2i.1 |
. . 3
![]() ![]() | |
4 | mp3an2i.4 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | mp3an1 1261 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 1, 2, 5 | syl2anc 404 |
1
![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 927 |
This theorem is referenced by: mapen 6616 mapxpen 6618 en2eleq 6882 nnledivrp 9298 frec2uzsucd 9869 seq3shft 10333 geolim2 10967 geoisum1c 10975 eflegeo 11053 sin01gt0 11113 cos01gt0 11114 gcdn0gt0 11308 divgcdodd 11461 sqpweven 11492 2sqpwodd 11493 ressid 11616 topnvalg 11725 |
Copyright terms: Public domain | W3C validator |