Metamath Proof Explorer


Theorem bj-axc14

Description: Alternate proof of axc14 (even when inlining the above results, this gives a shorter proof). (Contributed by BJ, 20-Oct-2021) (Proof modification is discouraged.)

Ref Expression
Assertion bj-axc14 ¬ z z = x ¬ z z = y x y z x y

Proof

Step Hyp Ref Expression
1 bj-axc14nf ¬ z z = x ¬ z z = y z x y
2 nf5r z x y x y z x y
3 2 a1i ¬ z z = x z x y x y z x y
4 1 3 syld ¬ z z = x ¬ z z = y x y z x y