Theorem eqeq2 2180

Description: Equality implies equivalence of equalities. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
eqeq2	|- ( A = B -> ( C = A <-> C = B ) )

Proof of Theorem eqeq2

Step	Hyp	Ref	Expression
1		eqeq1 2177	. 2 |- ( A = B -> ( A = C <-> B = C ) )
2		eqcom 2172	. 2 |- ( C = A <-> A = C )
3		eqcom 2172	. 2 |- ( C = B <-> B = C )
4	1, 2, 3	3bitr4g 222	1 |- ( A = B -> ( C = A <-> C = B ) )

Syntax hints:   -> wi 4   <-> wb 104   = wceq 1348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163

This theorem is referenced by:  eqeq2i  2181  eqeq2d  2182  eqeq12  2183  eleq1  2233  neeq2  2354  alexeq  2856  ceqex  2857  pm13.183  2868  eqeu  2900  mo2icl  2909  mob2  2910  euind  2917  reu6i  2921  reuind  2935  sbc5  2978  csbiebg  3091  sneq  3592  preqr1g  3751  preqr1  3753  prel12  3756  preq12bg  3758  opth  4220  euotd  4237  ordtriexmid  4503  ontriexmidim  4504  wetriext  4559  tfisi  4569  ideqg  4760  resieq  4899  cnveqb  5064  cnveq0  5065  iota5  5178  funopg  5230  fneq2  5285  foeq3  5416  tz6.12f  5523  funbrfv  5533  fnbrfvb  5535  fvelimab  5550  elrnrexdm  5633  eufnfv  5724  f1veqaeq  5746  mpoeq123  5910  ovmpt4g  5973  ovi3  5987  ovg  5989  caovcang  6012  caovcan  6015  frecabcl  6376  nntri3or  6470  dcdifsnid  6481  nnaordex  6505  nnawordex  6506  ereq2  6519  eroveu  6602  2dom  6781  fundmen  6782  xpf1o  6820  nneneq  6833  tridc  6875  fisseneq  6907  fidcenumlemrks  6928  supsnti  6980  isotilem  6981  updjud  7057  exmidontriimlem3  7193  exmidontriimlem4  7194  onntri35  7207  nqtri3or  7351  ltexnqq  7363  aptisr  7734  srpospr  7738  map2psrprg  7760  axpre-apti  7840  nntopi  7849  subval  8104  eqord1  8395  divvalap  8584  nn0ind-raph  9322  frecuzrdgtcl  10361  frecuzrdgfunlem  10368  sqrtrval  10957  summodclem2  11338  prodmodclem2  11533  divides  11744  dvdstr  11783  odd2np1lem  11824  ndvdssub  11882  eucalglt  12004  hashgcdeq  12186  ennnfonelemim  12372  dfgrp2  12725  xmeteq0  13118  trilpo  14040  trirec0  14041  redcwlpo  14052  redc0  14054  reap0  14055