Theorem eqeq12i 1897

Description: A useful inference for substituting definitions into an equality. (The proof was shortened by Andrew Salmon, 25-May-2011.)

Hypotheses

Ref	Expression
eqeq12i.1	|- A = B
eqeq12i.2	|- C = D

Assertion

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

Proof of Theorem eqeq12i

Step	Hyp	Ref	Expression
1		eqeq12i.1	. 2 |- A = B
2		eqeq12i.2	. 2 |- C = D
3		eqeq12 1896	. 2 |- ((A = B /\ C = D) -> (A = C <-> B = D))
4	1, 2, 3	mp2an 761	1 |- (A = C <-> B = D)

Syntax hints:   <-> wb 163   = wceq 1298

This theorem is referenced by:  sbceqdig 2554  sbceqdigOLD 2555  unineq 2844  preqr2 3153  opth 3532  rncoeq 4217  eqfnoprv 4945  ecopoprsym 5369  karden 5856  mulcmpblnq 6205  addcmpblnr 6333  ax1ne0 6433  addcani 6505  neg11i 6566  div11i 6940  rec11ii 6953  sq11i 7871  nn0opth2i 7917  sqr2irrlem4 7977  crui 7987  cjrebi 8031  ser0cji 8325  grpidval 9342  pjneli 11303  bnj549 13275  bnj1253 13470  bnj1283 13476  seq1resval 13617  seq1resval2 13618  algrp1 13742  eucalginv 13752  sspred 13886  wfrlem5 13961  sltval2 13997  axsltsolem1 14006  axfelem11 14041  axfelem16 14046  altopth1sn 14090  trooo 14758  vecval3b 14795  trhom 14983  ismona 15158  topbasfne 15499  seq1eq2 15817  iscring2 16146  compne 16417

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-17 1317  ax-4 1319  ax-5o 1321  ax-ext 1865

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

Copyright terms: Public domain