Theorem eqeqan12d 1487

Description: A useful inference for substituting definitions into an equality.

Hypotheses

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

Assertion

Ref	Expression
eqeqan12d	|- ((ph /\ ps) -> (A = C <-> B = D))

Proof of Theorem eqeqan12d

Step	Hyp	Ref	Expression
1		eqeqan12d.1	. . 3 |- (ph -> A = B)
2	1	adantr 389	. 2 |- ((ph /\ ps) -> A = B)
3		eqeqan12d.2	. . 3 |- (ps -> C = D)
4	3	adantl 388	. 2 |- ((ph /\ ps) -> C = D)
5	2, 4	eqeq12d 1486	1 |- ((ph /\ ps) -> (A = C <-> B = D))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   = wceq 954

This theorem is referenced by:  eqeqan12rd 1488  opth2 2795  tz7.48lem 3946  xpopth 4096  ecopopreq 4298  xpdom2 4428  unfilem2 4531  suc11reg 4585  addpipq 5034  mulpipq 5035  addsrpr 5164  mulsrpr 5165  cnegextlem1 5325  nnleltp1t 5909  zneo 6155  zneoOLD 6156  icoshftf1oi 6350  crutOLD 6677  cj11t 6773  recant 6850  reeff1 7358  efieq 7400  xpnnen 7449  znnen 7453  infmap2lem2 7530  grpinvf 8029  efifolem7 8662  efif1lem3 8666  efif1lem4 8667  efif1lem5 8668  efif1 8671  eff1i 8683  hial2eq2t 8912

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-17 969  ax-4 971  ax-5o 973  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-cleq 1467

Copyright terms: Public domain