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 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

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

This theorem is referenced by:  eqeqan12rd  2751  eqeq12d  2752  eqeq12  2753  eqfnfv2  6984  f1mpt  7216  soisores  7282  xpopth  7983  f1o2ndf1  8072  fnwelem  8081  fnse  8083  tz7.48lem  8380  ecopoveq  8765  xpdom2  9010  unfilem2  9216  wemaplem1  9461  suc11reg  9540  oemapval  9604  cantnf  9614  wemapwe  9618  r0weon  9934  infxpen  9936  fodomacn  9978  sornom  10199  fin1a2lem2  10323  fin1a2lem4  10325  neg11  11445  subeqrev  11572  rpnnen1lem6  12932  cnref1o  12935  xneg11  13167  injresinj  13746  modadd1  13867  modaddid  13869  modmul1  13886  modlteq  13907  sq11  14093  hashen  14309  fz1eqb  14316  eqwrd  14519  s111  14578  ccatopth  14678  wrd2ind  14685  wwlktovf1  14919  cj11  15124  sqrt11  15224  sqabs  15269  recan  15299  reeff1  16087  efieq  16130  eulerthlem2  16752  vdwlem12  16963  xpsff1o  17531  ismgmhm  18664  ismhm  18753  isghm  19190  gsmsymgreq  19407  symgfixf1  19412  odf1  19537  sylow1  19578  frgpuplem  19747  isdomn  20682  rngqiprngimfo  21299  pzriprnglem11  21471  cygznlem3  21549  psgnghm  21560  tgtop11  22947  fclsval  23973  vitali  25580  recosf1o  26499  mpodvdsmulf1o  27157  dvdsmulf1o  27159  fsumvma  27176  negs11  28041  oniso  28263  bdayn0sf1o  28362  brcgr  28969  axlowdimlem15  29025  axcontlem1  29033  axcontlem4  29036  axcontlem7  29039  axcontlem8  29040  iswlk  29679  wlkswwlksf1o  29947  wwlksnextinj  29967  clwlkclwwlkf1  30080  clwwlkf1  30119  numclwwlkqhash  30445  grpoinvf  30603  hial2eq2  31178  qusker  33409  bnj554  35041  erdszelem9  35381  sategoelfvb  35601  mrsubff1  35696  msubff1  35738  mvhf1  35741  fneval  36534  topfneec2  36538  bj-imdirval3  37498  f1omptsnlem  37652  f1omptsn  37653  rdgeqoa  37686  poimirlem4  37945  poimirlem26  37967  poimirlem27  37968  ismtyval  38121  extep  38610  brsucmap  38787  brdmqss  39051  disjimeceqim2  39126  qmapeldisjsim  39181  fimgmcyc  42979  sn-isghm  43106  wepwsolem  43470  fnwe2val  43477  aomclem8  43489  onsucf1o  43700  relexp0eq  44128  sprsymrelf1  47956  fmtnof1  47998  fmtnofac1  48033  prmdvdsfmtnof1  48050  sfprmdvdsmersenne  48066  gpgedgvtx0  48537  isupwlk  48612  uspgrsprf1  48623  2zlidl  48716  rrx2xpref1o  49194  rrx2plord  49196  rrx2plordisom  49199  sphere  49223  line2ylem  49227