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 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

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

This theorem is referenced by:  eqeqan12rd  2751  eqeq12d  2752  eqeq12  2753  eqfnfv2  6977  f1mpt  7207  soisores  7273  xpopth  7974  f1o2ndf1  8064  fnwelem  8073  fnse  8075  tz7.48lem  8372  ecopoveq  8755  xpdom2  9000  unfilem2  9206  wemaplem1  9451  suc11reg  9528  oemapval  9592  cantnf  9602  wemapwe  9606  r0weon  9922  infxpen  9924  fodomacn  9966  sornom  10187  fin1a2lem2  10311  fin1a2lem4  10313  neg11  11432  subeqrev  11559  rpnnen1lem6  12895  cnref1o  12898  xneg11  13130  injresinj  13707  modadd1  13828  modaddid  13830  modmul1  13847  modlteq  13868  sq11  14054  hashen  14270  fz1eqb  14277  eqwrd  14480  s111  14539  ccatopth  14639  wrd2ind  14646  wwlktovf1  14880  cj11  15085  sqrt11  15185  sqabs  15230  recan  15260  reeff1  16045  efieq  16088  eulerthlem2  16709  vdwlem12  16920  xpsff1o  17488  ismgmhm  18621  ismhm  18710  isghm  19144  gsmsymgreq  19361  symgfixf1  19366  odf1  19491  sylow1  19532  frgpuplem  19701  isdomn  20638  rngqiprngimfo  21256  pzriprnglem11  21446  cygznlem3  21524  psgnghm  21535  tgtop11  22926  fclsval  23952  vitali  25570  recosf1o  26500  mpodvdsmulf1o  27160  dvdsmulf1o  27162  fsumvma  27180  negs11  28045  oniso  28267  bdayn0sf1o  28366  brcgr  28973  axlowdimlem15  29029  axcontlem1  29037  axcontlem4  29040  axcontlem7  29043  axcontlem8  29044  iswlk  29684  wlkswwlksf1o  29952  wwlksnextinj  29972  clwlkclwwlkf1  30085  clwwlkf1  30124  numclwwlkqhash  30450  grpoinvf  30607  hial2eq2  31182  qusker  33430  bnj554  35055  erdszelem9  35393  sategoelfvb  35613  mrsubff1  35708  msubff1  35750  mvhf1  35753  fneval  36546  topfneec2  36550  bj-imdirval3  37389  f1omptsnlem  37541  f1omptsn  37542  rdgeqoa  37575  poimirlem4  37825  poimirlem26  37847  poimirlem27  37848  ismtyval  38001  extep  38482  brsucmap  38640  brdmqss  38904  fimgmcyc  42789  sn-isghm  42916  wepwsolem  43284  fnwe2val  43291  aomclem8  43303  onsucf1o  43514  relexp0eq  43942  sprsymrelf1  47742  fmtnof1  47781  fmtnofac1  47816  prmdvdsfmtnof1  47833  sfprmdvdsmersenne  47849  gpgedgvtx0  48307  isupwlk  48382  uspgrsprf1  48393  2zlidl  48486  rrx2xpref1o  48964  rrx2plord  48966  rrx2plordisom  48969  sphere  48993  line2ylem  48997