Theorem eqeqan12d 1482

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 1481	1 |- ((ph /\ ps) -> (A = C <-> B = D))

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

This theorem is referenced by:  eqeqan12rd 1483  opth2 2789  tz7.48lem 3940  xpopth 4090  ecopopreq 4292  xpdom2 4422  unfilem2 4525  suc11reg 4577  addpipq 5026  mulpipq 5027  addsrpr 5156  mulsrpr 5157  cnegextlem1 5317  nnleltp1t 5901  zneo 6147  zneoOLD 6148  icoshftf1oi 6342  crutOLD 6669  cj11t 6765  recant 6842  reeff1 7350  efieq 7392  xpnnen 7441  znnen 7445  infmap2lem2 7522  grpinvf 8014  efifolem7 8643  efif1lem3 8647  efif1lem4 8648  efif1lem5 8649  efif1 8652  eff1i 8665  hial2eq2t 8894

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