Metamath Proof Explorer


Theorem ax8

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 x = y x z y z

Proof

Step Hyp Ref Expression
1 equvinv x = y t t = x t = y
2 ax8v2 x = t x z t z
3 2 equcoms t = x x z t z
4 ax8v1 t = y t z y z
5 3 4 sylan9 t = x t = y x z y z
6 5 exlimiv t t = x t = y x z y z
7 1 6 sylbi x = y x z y z