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 x , z (resp. on y , z) does not permit, together with the other axioms, to prove reflexivity (resp. symmetry). (Contributed by BJ, 7-Dec-2020.)

Assertion

Ref	Expression
ax7	|- ( x = y -> ( x = z -> y = z ) )

Proof of Theorem ax7

Dummy variable t is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ax7v2 1938	. . . 4 |- ( x = t -> ( x = y -> t = y ) )
2		ax7v2 1938	. . . 4 |- ( x = t -> ( x = z -> t = z ) )
3		ax7v1 1937	. . . . . 6 |- ( t = y -> ( t = z -> y = z ) )
4	3	imp 445	. . . . 5 |- ( ( t = y /\ t = z ) -> y = z )
5	4	a1i 11	. . . 4 |- ( x = t -> ( ( t = y /\ t = z ) -> y = z ) )
6	1, 2, 5	syl2and 500	. . 3 |- ( x = t -> ( ( x = y /\ x = z ) -> y = z ) )
7	6	expd 452	. 2 |- ( x = t -> ( x = y -> ( x = z -> y = z ) ) )
8		ax6evr 1942	. 2 |- E. t x = t
9	7, 8	exlimiiv 1859	1 |- ( x = y -> ( x = z -> y = z ) )

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