Description: Lemma for jm2.27 . Expand existential quantifiers for reverse direction. (Contributed by Stefan O'Rear, 4-Oct-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | jm2.27a1 | |
|
jm2.27a2 | |
||
jm2.27a3 | |
||
jm2.27a4 | |
||
jm2.27a5 | |
||
jm2.27a6 | |
||
jm2.27a7 | |
||
jm2.27a8 | |
||
jm2.27a9 | |
||
jm2.27a10 | |
||
jm2.27a11 | |
||
jm2.27a12 | |
||
jm2.27a13 | |
||
jm2.27a14 | |
||
jm2.27a15 | |
||
jm2.27a16 | |
||
jm2.27a17 | |
||
jm2.27a18 | |
||
jm2.27a19 | |
||
jm2.27a20 | |
||
Assertion | jm2.27b | |