Theorem eqeqan12d 2750

Description: A useful inference for substituting definitions into an equality. See also eqeqan12dALT 2755. (Contributed by NM, 9-Aug-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.) Shorten other proofs. (Revised by Wolf Lammen, 23-Oct-2024.)

Hypotheses

Ref	Expression
eqeqan12d.1	⊢ (𝜑 → 𝐴 = 𝐵)
eqeqan12d.2	⊢ (𝜓 → 𝐶 = 𝐷)

Assertion

Ref	Expression
eqeqan12d	⊢ ((𝜑 ∧ 𝜓) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))

Proof of Theorem eqeqan12d

Step	Hyp	Ref	Expression
1		eqeqan12d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2	1	eqeq1d 2738	. 2 ⊢ (𝜑 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))
3		eqeqan12d.2	. . 3 ⊢ (𝜓 → 𝐶 = 𝐷)
4	3	eqeq2d 2747	. 2 ⊢ (𝜓 → (𝐵 = 𝐶 ↔ 𝐵 = 𝐷))
5	2, 4	sylan9bb 509	1 ⊢ ((𝜑 ∧ 𝜓) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2728

This theorem is referenced by:  eqeqan12rd  2751  eqeq12d  2752  eqeq12  2753  eqfnfv2  7027  f1mpt  7259  soisores  7325  xpopth  8034  f1o2ndf1  8126  fnwelem  8135  fnse  8137  tz7.48lem  8460  ecopoveq  8837  xpdom2  9086  unfilem2  9321  wemaplem1  9565  suc11reg  9638  oemapval  9702  cantnf  9712  wemapwe  9716  r0weon  10031  infxpen  10033  fodomacn  10075  sornom  10296  fin1a2lem2  10420  fin1a2lem4  10422  neg11  11539  subeqrev  11664  rpnnen1lem6  13003  cnref1o  13006  xneg11  13236  injresinj  13809  modadd1  13930  modmul1  13947  modlteq  13968  sq11  14154  hashen  14370  fz1eqb  14377  eqwrd  14580  s111  14638  ccatopth  14739  wrd2ind  14746  wwlktovf1  14981  cj11  15186  sqrt11  15286  sqabs  15331  recan  15360  reeff1  16143  efieq  16186  eulerthlem2  16806  vdwlem12  17017  xpsff1o  17586  ismgmhm  18679  ismhm  18768  isghm  19203  gsmsymgreq  19418  symgfixf1  19423  odf1  19548  sylow1  19589  frgpuplem  19758  isdomn  20670  rngqiprngimfo  21267  pzriprnglem11  21457  cygznlem3  21535  psgnghm  21545  tgtop11  22925  fclsval  23951  vitali  25571  recosf1o  26501  mpodvdsmulf1o  27161  dvdsmulf1o  27163  fsumvma  27181  negs11  28012  onsiso  28226  bdayn0sf1o  28316  brcgr  28884  axlowdimlem15  28940  axcontlem1  28948  axcontlem4  28951  axcontlem7  28954  axcontlem8  28955  iswlk  29595  wlkswwlksf1o  29866  wwlksnextinj  29886  clwlkclwwlkf1  29996  clwwlkf1  30035  numclwwlkqhash  30361  grpoinvf  30518  hial2eq2  31093  qusker  33369  bnj554  34935  erdszelem9  35226  sategoelfvb  35446  mrsubff1  35541  msubff1  35583  mvhf1  35586  fneval  36375  topfneec2  36379  bj-imdirval3  37207  f1omptsnlem  37359  f1omptsn  37360  rdgeqoa  37393  poimirlem4  37653  poimirlem26  37675  poimirlem27  37676  ismtyval  37829  extep  38306  brdmqss  38669  fimgmcyc  42532  sn-isghm  42671  wepwsolem  43041  fnwe2val  43048  aomclem8  43060  onsucf1o  43271  relexp0eq  43700  sprsymrelf1  47490  fmtnof1  47529  fmtnofac1  47564  prmdvdsfmtnof1  47581  sfprmdvdsmersenne  47597  gpgedgvtx0  48045  isupwlk  48091  uspgrsprf1  48102  2zlidl  48195  rrx2xpref1o  48678  rrx2plord  48680  rrx2plordisom  48683  sphere  48707  line2ylem  48711