![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mp3an2i | Unicode version |
Description: mp3an 1337 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 1324 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 1, 2, 5 | syl2anc 411 |
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: mapen 6848 mapxpen 6850 en2eleq 7196 nnledivrp 9768 xsubge0 9883 iccen 10008 frec2uzsucd 10403 seq3shft 10849 geolim2 11522 geoisum1c 11530 ntrivcvgap 11558 eflegeo 11711 sin01gt0 11771 cos01gt0 11772 gcdn0gt0 11981 uzwodc 12040 divgcdodd 12145 sqpweven 12177 2sqpwodd 12178 pythagtriplem4 12270 pythagtriplem11 12276 pythagtriplem12 12277 pythagtriplem13 12278 pythagtriplem14 12279 pcfac 12350 omctfn 12446 ssnnctlemct 12449 topnvalg 12705 imasmulr 12735 imasaddfnlemg 12740 ismhm 12858 scaffng 13404 lss1d 13475 zringinvg 13579 restbasg 13753 restco 13759 lmfval 13777 cnfval 13779 cnpval 13783 upxp 13857 uptx 13859 txrest 13861 xblm 14002 bdmet 14087 bdmopn 14089 reopnap 14123 cnopnap 14179 dvidlemap 14245 dvcj 14258 eflt 14281 logdivlti 14387 trilpolemisumle 14871 |
Copyright terms: Public domain | W3C validator |