Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mp3an2i | Unicode version |
Description: mp3an 1319 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 1306 | . 2 |
6 | 1, 2, 5 | syl2anc 409 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 w3a 963 |
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 965 |
This theorem is referenced by: mapen 6788 mapxpen 6790 en2eleq 7125 nnledivrp 9668 xsubge0 9780 iccen 9905 frec2uzsucd 10295 seq3shft 10733 geolim2 11404 geoisum1c 11412 ntrivcvgap 11440 eflegeo 11593 sin01gt0 11653 cos01gt0 11654 gcdn0gt0 11856 divgcdodd 12012 sqpweven 12044 2sqpwodd 12045 omctfn 12159 ssnnctlemct 12162 ressid 12238 topnvalg 12350 restbasg 12555 restco 12561 lmfval 12579 cnfval 12581 cnpval 12585 upxp 12659 uptx 12661 txrest 12663 xblm 12804 bdmet 12889 bdmopn 12891 reopnap 12925 cnopnap 12981 dvidlemap 13047 dvcj 13060 eflt 13083 logdivlti 13189 trilpolemisumle 13596 |
Copyright terms: Public domain | W3C validator |