Theorem eqeqan12d 1533

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

Hypotheses

Ref	Expression
eqeqan12d.1	⊢ (φ → A = B)
eqeqan12d.2	⊢ (ψ → C = D)

Assertion

Ref	Expression
eqeqan12d	⊢ ((φ ⋀ ψ) → (A = C ↔ B = D))

Proof of Theorem eqeqan12d

Step	Hyp	Ref	Expression
1		eqeqan12d.1	. . 3 ⊢ (φ → A = B)
2	1	adantr 389	. 2 ⊢ ((φ ⋀ ψ) → A = B)
3		eqeqan12d.2	. . 3 ⊢ (ψ → C = D)
4	3	adantl 388	. 2 ⊢ ((φ ⋀ ψ) → C = D)
5	2, 4	eqeq12d 1532	1 ⊢ ((φ ⋀ ψ) → (A = C ↔ B = D))

Syntax hints:   → wi 3   ↔ wb 144   ⋀ wa 221   = wceq 992

This theorem is referenced by:  eqeqan12rd 1534  opth2 2876  xpopth 4166  tz7.48lem 4256  ecopopreq 4449  xpdom2 4583  unfilem2 4695  suc11reg 4750  addpipq 5208  mulpipq 5209  addsrpr 5338  mulsrpr 5339  cnegexlem1 5499  nnleltp1 6100  zneo 6371  modadd1 6477  modmul1 6478  icoshftf1oii 6536  cj11 7031  cj11OLD 7032  sqabs 7071  recan 7108  reeff1 7618  efieq 7658  xpnnen 7711  znnen 7714  infmap2lem2 7792  grpinvf 8297  efifolem7 9000  efif1lem3 9004  efif1lem4 9005  efif1lem5 9006  efif1 9009  eff1i 9016  hial2eq2 9249  ismrer1 12080

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 999  ax-17 1007  ax-4 1009  ax-5o 1011  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-an 223  df-cleq 1511

Copyright terms: Public domain