Step 
Hyp 
Ref 
Expression 
1 

equvinv 
⊢ ( 𝑦 = 𝑧 ↔ ∃ 𝑤 ( 𝑤 = 𝑦 ∧ 𝑤 = 𝑧 ) ) 
2 

ax13lem1 
⊢ ( ¬ 𝑥 = 𝑦 → ( 𝑤 = 𝑦 → ∀ 𝑥 𝑤 = 𝑦 ) ) 
3 
2

imp 
⊢ ( ( ¬ 𝑥 = 𝑦 ∧ 𝑤 = 𝑦 ) → ∀ 𝑥 𝑤 = 𝑦 ) 
4 

ax13lem1 
⊢ ( ¬ 𝑥 = 𝑧 → ( 𝑤 = 𝑧 → ∀ 𝑥 𝑤 = 𝑧 ) ) 
5 
4

imp 
⊢ ( ( ¬ 𝑥 = 𝑧 ∧ 𝑤 = 𝑧 ) → ∀ 𝑥 𝑤 = 𝑧 ) 
6 

ax7v1 
⊢ ( 𝑤 = 𝑦 → ( 𝑤 = 𝑧 → 𝑦 = 𝑧 ) ) 
7 
6

imp 
⊢ ( ( 𝑤 = 𝑦 ∧ 𝑤 = 𝑧 ) → 𝑦 = 𝑧 ) 
8 
7

alanimi 
⊢ ( ( ∀ 𝑥 𝑤 = 𝑦 ∧ ∀ 𝑥 𝑤 = 𝑧 ) → ∀ 𝑥 𝑦 = 𝑧 ) 
9 
3 5 8

syl2an 
⊢ ( ( ( ¬ 𝑥 = 𝑦 ∧ 𝑤 = 𝑦 ) ∧ ( ¬ 𝑥 = 𝑧 ∧ 𝑤 = 𝑧 ) ) → ∀ 𝑥 𝑦 = 𝑧 ) 
10 
9

an4s 
⊢ ( ( ( ¬ 𝑥 = 𝑦 ∧ ¬ 𝑥 = 𝑧 ) ∧ ( 𝑤 = 𝑦 ∧ 𝑤 = 𝑧 ) ) → ∀ 𝑥 𝑦 = 𝑧 ) 
11 
10

ex 
⊢ ( ( ¬ 𝑥 = 𝑦 ∧ ¬ 𝑥 = 𝑧 ) → ( ( 𝑤 = 𝑦 ∧ 𝑤 = 𝑧 ) → ∀ 𝑥 𝑦 = 𝑧 ) ) 
12 
11

exlimdv 
⊢ ( ( ¬ 𝑥 = 𝑦 ∧ ¬ 𝑥 = 𝑧 ) → ( ∃ 𝑤 ( 𝑤 = 𝑦 ∧ 𝑤 = 𝑧 ) → ∀ 𝑥 𝑦 = 𝑧 ) ) 
13 
1 12

syl5bi 
⊢ ( ( ¬ 𝑥 = 𝑦 ∧ ¬ 𝑥 = 𝑧 ) → ( 𝑦 = 𝑧 → ∀ 𝑥 𝑦 = 𝑧 ) ) 
14 
13

ex 
⊢ ( ¬ 𝑥 = 𝑦 → ( ¬ 𝑥 = 𝑧 → ( 𝑦 = 𝑧 → ∀ 𝑥 𝑦 = 𝑧 ) ) ) 
15 

ax13b 
⊢ ( ( ¬ 𝑥 = 𝑦 → ( 𝑦 = 𝑧 → ∀ 𝑥 𝑦 = 𝑧 ) ) ↔ ( ¬ 𝑥 = 𝑦 → ( ¬ 𝑥 = 𝑧 → ( 𝑦 = 𝑧 → ∀ 𝑥 𝑦 = 𝑧 ) ) ) ) 
16 
14 15

mpbir 
⊢ ( ¬ 𝑥 = 𝑦 → ( 𝑦 = 𝑧 → ∀ 𝑥 𝑦 = 𝑧 ) ) 