Theorem ax7 1943

Description: Proof of ax-7 1935 from ax7v1 1937 and ax7v2 1938, proving sufficiency of the conjunction of the latter two weakened versions of ax7v 1936, which is itself a weakened version of ax-7 1935.

Note that the weakened version of ax-7 1935 obtained by adding a dv condition on 𝑥, 𝑧 (resp. on 𝑦, 𝑧) does not permit, together with the other axioms, to prove reflexivity (resp. symmetry). (Contributed by BJ, 7-Dec-2020.)

Assertion

Ref	Expression
ax7	⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧))

Proof of Theorem ax7

Dummy variable 𝑡 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ax7v2 1938	. . . 4 ⊢ (𝑥 = 𝑡 → (𝑥 = 𝑦 → 𝑡 = 𝑦))
2		ax7v2 1938	. . . 4 ⊢ (𝑥 = 𝑡 → (𝑥 = 𝑧 → 𝑡 = 𝑧))
3		ax7v1 1937	. . . . . 6 ⊢ (𝑡 = 𝑦 → (𝑡 = 𝑧 → 𝑦 = 𝑧))
4	3	imp 445	. . . . 5 ⊢ ((𝑡 = 𝑦 ∧ 𝑡 = 𝑧) → 𝑦 = 𝑧)
5	4	a1i 11	. . . 4 ⊢ (𝑥 = 𝑡 → ((𝑡 = 𝑦 ∧ 𝑡 = 𝑧) → 𝑦 = 𝑧))
6	1, 2, 5	syl2and 500	. . 3 ⊢ (𝑥 = 𝑡 → ((𝑥 = 𝑦 ∧ 𝑥 = 𝑧) → 𝑦 = 𝑧))
7	6	expd 452	. 2 ⊢ (𝑥 = 𝑡 → (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧)))
8		ax6evr 1942	. 2 ⊢ ∃𝑡 𝑥 = 𝑡
9	7, 8	exlimiiv 1859	1 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧))

Syntax hints:   → wi 4   ∧ wa 384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705

This theorem is referenced by:  equcomi  1944  equtr  1948  equequ1  1952  equvinv  1959  cbvaev  1979  aeveq  1982  aevOLD  2162  aevALTOLD  2321  axc16i  2322  equvel  2347  axext3  2604  dtru  4857  axextnd  9413  bj-dtru  32797  bj-mo3OLD  32832  wl-aetr  33317  wl-exeq  33321  wl-aleq  33322  wl-nfeqfb  33323  equcomi1  34185  hbequid  34194  equidqe  34207  aev-o  34216  ax6e2eq  38773  ax6e2eqVD  39143