Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mp3an2i | Unicode version |
Description: mp3an 1332 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 1319 | . 2 |
6 | 1, 2, 5 | syl2anc 409 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 w3a 973 |
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 975 |
This theorem is referenced by: mapen 6824 mapxpen 6826 en2eleq 7172 nnledivrp 9723 xsubge0 9838 iccen 9963 frec2uzsucd 10357 seq3shft 10802 geolim2 11475 geoisum1c 11483 ntrivcvgap 11511 eflegeo 11664 sin01gt0 11724 cos01gt0 11725 gcdn0gt0 11933 uzwodc 11992 divgcdodd 12097 sqpweven 12129 2sqpwodd 12130 pythagtriplem4 12222 pythagtriplem11 12228 pythagtriplem12 12229 pythagtriplem13 12230 pythagtriplem14 12231 pcfac 12302 omctfn 12398 ssnnctlemct 12401 ressid 12479 topnvalg 12591 ismhm 12685 restbasg 12962 restco 12968 lmfval 12986 cnfval 12988 cnpval 12992 upxp 13066 uptx 13068 txrest 13070 xblm 13211 bdmet 13296 bdmopn 13298 reopnap 13332 cnopnap 13388 dvidlemap 13454 dvcj 13467 eflt 13490 logdivlti 13596 trilpolemisumle 14070 |
Copyright terms: Public domain | W3C validator |