Theorem eqeqan12d 2749

Description: A useful inference for substituting definitions into an equality. See also eqeqan12dALT 2757. (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 2737	. 2 ⊢ (𝜑 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))
3		eqeqan12d.2	. . 3 ⊢ (𝜓 → 𝐶 = 𝐷)
4	3	eqeq2d 2746	. 2 ⊢ (𝜓 → (𝐵 = 𝐶 ↔ 𝐵 = 𝐷))
5	2, 4	sylan9bb 509	1 ⊢ ((𝜑 ∧ 𝜓) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727

This theorem is referenced by:  eqeqan12rd  2750  eqeq12d  2751  eqeq12  2752  eqfnfv2  7052  f1mpt  7281  soisores  7347  xpopth  8054  f1o2ndf1  8146  fnwelem  8155  fnse  8157  tz7.48lem  8480  ecopoveq  8857  xpdom2  9106  unfilem2  9342  wemaplem1  9584  suc11reg  9657  oemapval  9721  cantnf  9731  wemapwe  9735  r0weon  10050  infxpen  10052  fodomacn  10094  sornom  10315  fin1a2lem2  10439  fin1a2lem4  10441  neg11  11558  subeqrev  11683  rpnnen1lem6  13022  cnref1o  13025  xneg11  13254  injresinj  13824  modadd1  13945  modmul1  13962  modlteq  13983  sq11  14168  hashen  14383  fz1eqb  14390  eqwrd  14592  s111  14650  ccatopth  14751  wrd2ind  14758  wwlktovf1  14993  cj11  15198  sqrt11  15298  sqabs  15343  recan  15372  reeff1  16153  efieq  16196  eulerthlem2  16816  vdwlem12  17026  xpsff1o  17614  ismgmhm  18722  ismhm  18811  isghm  19246  gsmsymgreq  19465  symgfixf1  19470  odf1  19595  sylow1  19636  frgpuplem  19805  isdomn  20722  rngqiprngimfo  21329  pzriprnglem11  21520  cygznlem3  21606  psgnghm  21616  tgtop11  23005  fclsval  24032  vitali  25662  recosf1o  26592  mpodvdsmulf1o  27252  dvdsmulf1o  27254  fsumvma  27272  negs11  28096  brcgr  28930  axlowdimlem15  28986  axcontlem1  28994  axcontlem4  28997  axcontlem7  29000  axcontlem8  29001  iswlk  29643  wlkswwlksf1o  29909  wwlksnextinj  29929  clwlkclwwlkf1  30039  clwwlkf1  30078  numclwwlkqhash  30404  grpoinvf  30561  hial2eq2  31136  qusker  33357  bnj554  34892  erdszelem9  35184  sategoelfvb  35404  mrsubff1  35499  msubff1  35541  mvhf1  35544  fneval  36335  topfneec2  36339  bj-imdirval3  37167  f1omptsnlem  37319  f1omptsn  37320  rdgeqoa  37353  poimirlem4  37611  poimirlem26  37633  poimirlem27  37634  ismtyval  37787  extep  38265  brdmqss  38628  fimgmcyc  42521  sn-isghm  42660  wepwsolem  43031  fnwe2val  43038  aomclem8  43050  onsucf1o  43262  relexp0eq  43691  sprsymrelf1  47421  fmtnof1  47460  fmtnofac1  47495  prmdvdsfmtnof1  47512  sfprmdvdsmersenne  47528  gpgedgvtx0  47954  isupwlk  47980  uspgrsprf1  47991  2zlidl  48084  rrx2xpref1o  48568  rrx2plord  48570  rrx2plordisom  48573  sphere  48597  line2ylem  48601