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 ( ¬ ∀ 𝑧 𝑧 = 𝑥 → ( ¬ ∀ 𝑧 𝑧 = 𝑦 → ( 𝑥𝑦 → ∀ 𝑧 𝑥𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 bj-axc14nf ( ¬ ∀ 𝑧 𝑧 = 𝑥 → ( ¬ ∀ 𝑧 𝑧 = 𝑦 → Ⅎ 𝑧 𝑥𝑦 ) )
2 nf5r ( Ⅎ 𝑧 𝑥𝑦 → ( 𝑥𝑦 → ∀ 𝑧 𝑥𝑦 ) )
3 2 a1i ( ¬ ∀ 𝑧 𝑧 = 𝑥 → ( Ⅎ 𝑧 𝑥𝑦 → ( 𝑥𝑦 → ∀ 𝑧 𝑥𝑦 ) ) )
4 1 3 syld ( ¬ ∀ 𝑧 𝑧 = 𝑥 → ( ¬ ∀ 𝑧 𝑧 = 𝑦 → ( 𝑥𝑦 → ∀ 𝑧 𝑥𝑦 ) ) )