Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > mp3an2i | Structured version Visualization version Unicode version |
Description: mp3an 1424 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 1411 | . 2 |
6 | 1, 2, 5 | syl2anc 693 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 w3a 1037 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 197 df-an 386 df-3an 1039 |
This theorem is referenced by: nnledivrp 11940 wrdlen2i 13686 0.999... 14612 fsumcube 14791 3dvds 15052 divgcdodd 15422 cnaddinv 18274 opsrtoslem2 19485 frgpcyg 19922 pt1hmeo 21609 cnheiborlem 22753 lgsqrlem4 25074 gausslemma2dlem4 25094 lgsquad2lem2 25110 wlkp1lem3 26572 wlkp1lem7 26576 wlkp1lem8 26577 pthdlem1 26662 conngrv2edg 27055 cvmlift2lem10 31294 nosupbday 31851 enrelmap 38291 k0004lem3 38447 sineq0ALT 39173 xlimconst 40051 odz2prm2pw 41475 fmtno4prmfac 41484 lighneallem3 41524 lighneallem4a 41525 lighneallem4 41527 |
Copyright terms: Public domain | W3C validator |