Description: Lemma 1 for pm2mpmhm . (Contributed by AV, 21-Oct-2019) (Revised by AV, 6-Dec-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | pm2mpfo.p | |
|
pm2mpfo.c | |
||
pm2mpfo.b | |
||
pm2mpfo.m | |
||
pm2mpfo.e | |
||
pm2mpfo.x | |
||
pm2mpfo.a | |
||
pm2mpfo.q | |
||
pm2mpfo.l | |
||
pm2mpfo.t | |
||
Assertion | pm2mpmhmlem1 | |