Theorem eqeqan12d 1901

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

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		eqeq12 1896	. 2 |- ((A = B /\ C = D) -> (A = C <-> B = D))
2		eqeqan12d.1	. 2 |- (ph -> A = B)
3		eqeqan12d.2	. 2 |- (ps -> C = D)
4	1, 2, 3	syl2an 503	1 |- ((ph /\ ps) -> (A = C <-> B = D))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   = wceq 1298

This theorem is referenced by:  eqeqan12rd 1903  opth2 3546  xpopth 5046  tz7.48lem 5164  ecopopreq 5367  xpdom2 5501  unfilem2 5642  suc11reg 5710  addpipq 6206  mulpipq 6207  addsrpr 6336  mulsrpr 6337  cnegexlem1 6499  nnleltp1 7138  zneo 7412  modadd1 7518  modmul1 7519  icoshftf1oii 7578  cj11 8080  cj11OLD 8081  sqabs 8120  recan 8157  hashen 8233  reeff1 8675  efieq 8715  xpnnen 8768  znnen 8771  infmap2lem2 8849  grpinvf 9364  efifolem7 10082  efif1lem3 10086  efif1lem4 10087  efif1lem5 10088  efif1 10091  eff1i 10098  hial2eq2 10606  bnj550 13276  axdenselem5 14023  gaplc 14731  ismrer1 16024

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