Theorem equequ1 1798

Description: An equivalence law for equality. (Contributed by NM, 1-Aug-1993.) (Proof shortened by Wolf Lammen, 10-Dec-2017.)

Assertion

Ref	Expression
equequ1

Proof of Theorem equequ1

Step	Hyp	Ref	Expression
1		ax-7 1790	. 2
2		equtr 1796	. 2
3	1, 2	impbid 191	1

Syntax hints:  ->wi 4  <->wb 184

This theorem is referenced by:  equequ2  1799  drsb1  2118  equsb3lem  2175  dveeq1-o  2265  dveeq1-o16  2266  axc11n-16  2268  ax12eq  2271  sb8eu  2318  2eu6OLD  2384  euequ1OLD  2387  axext3OLD  2438  reu6  3288  reu7  3294  disjxun  4450  cbviota  5561  dff13f  6167  poxp  6912  unxpdomlem1  7744  unxpdomlem2  7745  aceq0  8520  zfac  8861  axrepndlem1  8988  axpowndlem2OLD  8995  zfcndac  9018  injresinj  11926  fsum2dlem  13585  ramub1lem2  14545  ramcl  14547  symgextf1  16446  mamulid  18943  mamurid  18944  mdetdiagid  19102  mdetunilem9  19122  alexsubALTlem3  20549  ptcmplem2  20553  dscmet  21093  dyadmbllem  22008  opnmbllem  22010  isppw2  23389  frg2wot1  25057  disji2f  27438  disjif2  27442  ghomf1olem  29034  wl-equsb3  30004  mblfinlem1  30051  bfp  30320  fphpd  30750  lcoss  33037  ax6e2nd  33331  ax6e2ndVD  33708  ax6e2ndALT  33730  bj-axext3  34354

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790

This theorem depends on definitions:  df-bi 185  df-ex 1613