Theorem eqeq12d 2367

Description: A useful inference for substituting definitions into an equality. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Hypotheses

Ref	Expression
eqeq12d.1	|- (ph -> A = B)
eqeq12d.2	|- (ph -> C = D)

Assertion

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

Proof of Theorem eqeq12d

Step	Hyp	Ref	Expression
1		eqeq12d.1	. 2 |- (ph -> A = B)
2		eqeq12d.2	. 2 |- (ph -> C = D)
3		eqeq12 2365	. 2 |- ((A = B /\ C = D) -> (A = C <-> B = D))
4	1, 2, 3	syl2anc 642	1 |- (ph -> (A = C <-> B = D))

Syntax hints:   -> wi 4   <-> wb 176   = wceq 1642

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-cleq 2346

This theorem is referenced by:  sbceqg  3153  csbing  3463  csbifg  3691  uniprg  3907  unisng  3909  intprg  3961  iununi  4051  csbiotag  4372  preaddccan2  4456  csbopabg  4638  csbima12g  4956  fveqres  5356  eqfnfv2f  5397  fvreseq  5399  fnressn  5439  fvi  5443  fvsng  5447  csbovg  5553  eqfnov  5590  ov2ag  5599  caovcomg  5625  caovassg  5627  caovcan  5629  caovdig  5633  caovdirg  5634  caovmo  5646  ov2gf  5712  fvmptf  5723  fvfullfun  5865  taddc  6230  letc  6232  addcdi  6251  addccan2nc  6266  nchoicelem1  6290  nchoicelem2  6291  nchoicelem9  6298  nchoicelem17  6306  nchoice  6309