Description: Proof of ax-8 from ax8v1 and ax8v2 , proving sufficiency of the conjunction of the latter two weakened versions of ax8v , which is itself a weakened version of ax-8 . (Contributed by BJ, 7-Dec-2020) (Proof shortened by Wolf Lammen, 11-Apr-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | ax8 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | equvinv | ||
2 | ax8v2 | ||
3 | 2 | equcoms | |
4 | ax8v1 | ||
5 | 3 4 | sylan9 | |
6 | 5 | exlimiv | |
7 | 1 6 | sylbi |