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=yxzyz

Proof

Step Hyp Ref Expression
1 equvinv x=ytt=xt=y
2 ax8v2 x=txztz
3 2 equcoms t=xxztz
4 ax8v1 t=ytzyz
5 3 4 sylan9 t=xt=yxzyz
6 5 exlimiv tt=xt=yxzyz
7 1 6 sylbi x=yxzyz