Theorem equequ2 1495

Description: An equivalence law for equality.

Assertion

Ref	Expression
equequ2	|- (x = y -> (z = x <-> z = y))

Proof of Theorem equequ2

Step	Hyp	Ref	Expression
1		equtrr 1491	. 2 |- (x = y -> (z = x -> z = y))
2		equtrr 1491	. . 3 |- (y = x -> (z = y -> z = x))
3	2	equcoms 1489	. 2 |- (x = y -> (z = y -> z = x))
4	1, 3	impbid 574	1 |- (x = y -> (z = x <-> z = y))

Syntax hints:   -> wi 3   <-> wb 163   = wceq 1298

This theorem is referenced by:  dveeq2 1582  dveeq2ALT 1583  ax11v2 1585  sb7fOLD 1732  ax11eq 1754  ax11inda 1762  eujust 1773  eujustALT 1774  euf 1777  mo 1787  2mo 1851  2eu6 1858  axrep2 3430  dtru 3498  zfpair 3522  dfid3 3587  dfwe2 3861  asymref2OLD 4311  fparlem3 5083  fparlem4 5084  iotaval 5096  aceq0 5892  zfac 5907  axpowndlem4 6104  zfcndac 6123  dscmet 9196  ax10-16 16365  iotavalb 16394

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-8 1306  ax-12 1310  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481

This theorem depends on definitions:  df-bi 164  df-an 242

Copyright terms: Public domain