HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem eqeq12i 1480
Description: A useful inference for substituting definitions into an equality.
Hypotheses
Ref Expression
eqeq12i.1 |- A = B
eqeq12i.2 |- C = D
Assertion
Ref Expression
eqeq12i |- (A = C <-> B = D)
Proof of Theorem eqeq12i
StepHypRef Expression
1 eqeq12i.1 . . 3 |- A = B
21eqeq1i 1474 . 2 |- (A = C <-> B = C)
3 eqeq12i.2 . . 3 |- C = D
43eqeq2i 1477 . 2 |- (B = C <-> B = D)
52, 4bitr 173 1 |- (A = C <-> B = D)
Colors of variables: wff set class
Syntax hints:   <-> wb 146   = wceq 953
This theorem is referenced by:  sbceqdig 2002  unineq 2245  preqr2 2473  opth 2777  rncoeq 3351  eqfnoprval 4001  ecopoprsym 4294  karden 4698  mulcmpblnq 5025  addcmpblnr 5153  ax1ne0 5252  neg11 5378  div11 5720  rec11i 5733  sq11 6557  nn0opth2 6597  sqr2irrlem4 6657  cru 6667  cjreb 6716  ser0cj 7003  pjnel 9585  ismona 10579
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972  ax-ext 1452
This theorem depends on definitions:  df-bi 147  df-an 225  df-cleq 1462
Copyright terms: Public domain