Theorem eqeqan12d 2747

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 2735	. 2 ⊢ (𝜑 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))
3		eqeqan12d.2	. . 3 ⊢ (𝜓 → 𝐶 = 𝐷)
4	3	eqeq2d 2744	. 2 ⊢ (𝜓 → (𝐵 = 𝐶 ↔ 𝐵 = 𝐷))
5	2, 4	sylan9bb 511	1 ⊢ ((𝜑 ∧ 𝜓) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725

This theorem is referenced by:  eqeqan12rd  2748  eqeq12d  2749  eqeq12  2750  eqfnfv2  7034  f1mpt  7260  soisores  7324  xpopth  8016  f1o2ndf1  8108  fnwelem  8117  fnse  8119  tz7.48lem  8441  ecopoveq  8812  xpdom2  9067  unfilem2  9311  wemaplem1  9541  suc11reg  9614  oemapval  9678  cantnf  9688  wemapwe  9692  r0weon  10007  infxpen  10009  fodomacn  10051  sornom  10272  fin1a2lem2  10396  fin1a2lem4  10398  neg11  11511  subeqrev  11636  rpnnen1lem6  12966  cnref1o  12969  xneg11  13194  injresinj  13753  modadd1  13873  modmul1  13889  modlteq  13910  sq11  14096  hashen  14307  fz1eqb  14314  eqwrd  14507  s111  14565  ccatopth  14666  wrd2ind  14673  wwlktovf1  14908  cj11  15109  sqrt11  15209  sqabs  15254  recan  15283  reeff1  16063  efieq  16106  eulerthlem2  16715  vdwlem12  16925  xpsff1o  17513  ismhm  18673  gsmsymgreq  19300  symgfixf1  19305  odf1  19430  sylow1  19471  frgpuplem  19640  isdomn  20910  cygznlem3  21125  psgnghm  21133  tgtop11  22485  fclsval  23512  vitali  25130  recosf1o  26044  dvdsmulf1o  26698  fsumvma  26716  negs11  27523  brcgr  28158  axlowdimlem15  28214  axcontlem1  28222  axcontlem4  28225  axcontlem7  28228  axcontlem8  28229  iswlk  28867  wlkswwlksf1o  29133  wwlksnextinj  29153  clwlkclwwlkf1  29263  clwwlkf1  29302  numclwwlkqhash  29628  grpoinvf  29785  hial2eq2  30360  qusker  32464  bnj554  33910  erdszelem9  34190  sategoelfvb  34410  mrsubff1  34505  msubff1  34547  mvhf1  34550  fneval  35237  topfneec2  35241  bj-imdirval3  36065  f1omptsnlem  36217  f1omptsn  36218  rdgeqoa  36251  poimirlem4  36492  poimirlem26  36514  poimirlem27  36515  ismtyval  36668  extep  37151  brdmqss  37516  wepwsolem  41784  fnwe2val  41791  aomclem8  41803  onsucf1o  42022  relexp0eq  42452  sprsymrelf1  46164  fmtnof1  46203  fmtnofac1  46238  prmdvdsfmtnof1  46255  sfprmdvdsmersenne  46271  isupwlk  46514  uspgrsprf1  46525  ismgmhm  46553  rngqiprngimfo  46786  pzriprnglem11  46815  2zlidl  46832  rrx2xpref1o  47404  rrx2plord  47406  rrx2plordisom  47409  sphere  47433  line2ylem  47437