Theorem eqeqan12d 2748

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-cleq 2726

This theorem is referenced by:  eqeqan12rd  2749  eqeq12d  2750  eqeq12  2751  eqfnfv2  7032  f1mpt  7263  soisores  7329  xpopth  8037  f1o2ndf1  8129  fnwelem  8138  fnse  8140  tz7.48lem  8463  ecopoveq  8840  xpdom2  9089  unfilem2  9326  wemaplem1  9568  suc11reg  9641  oemapval  9705  cantnf  9715  wemapwe  9719  r0weon  10034  infxpen  10036  fodomacn  10078  sornom  10299  fin1a2lem2  10423  fin1a2lem4  10425  neg11  11542  subeqrev  11667  rpnnen1lem6  13006  cnref1o  13009  xneg11  13239  injresinj  13809  modadd1  13930  modmul1  13947  modlteq  13968  sq11  14153  hashen  14368  fz1eqb  14375  eqwrd  14577  s111  14635  ccatopth  14736  wrd2ind  14743  wwlktovf1  14978  cj11  15183  sqrt11  15283  sqabs  15328  recan  15357  reeff1  16138  efieq  16181  eulerthlem2  16801  vdwlem12  17012  xpsff1o  17583  ismgmhm  18678  ismhm  18767  isghm  19202  gsmsymgreq  19418  symgfixf1  19423  odf1  19548  sylow1  19589  frgpuplem  19758  isdomn  20673  rngqiprngimfo  21273  pzriprnglem11  21464  cygznlem3  21542  psgnghm  21552  tgtop11  22936  fclsval  23962  vitali  25584  recosf1o  26513  mpodvdsmulf1o  27173  dvdsmulf1o  27175  fsumvma  27193  negs11  28017  brcgr  28845  axlowdimlem15  28901  axcontlem1  28909  axcontlem4  28912  axcontlem7  28915  axcontlem8  28916  iswlk  29556  wlkswwlksf1o  29827  wwlksnextinj  29847  clwlkclwwlkf1  29957  clwwlkf1  29996  numclwwlkqhash  30322  grpoinvf  30479  hial2eq2  31054  qusker  33312  bnj554  34872  erdszelem9  35163  sategoelfvb  35383  mrsubff1  35478  msubff1  35520  mvhf1  35523  fneval  36312  topfneec2  36316  bj-imdirval3  37144  f1omptsnlem  37296  f1omptsn  37297  rdgeqoa  37330  poimirlem4  37590  poimirlem26  37612  poimirlem27  37613  ismtyval  37766  extep  38243  brdmqss  38606  fimgmcyc  42507  sn-isghm  42646  wepwsolem  43017  fnwe2val  43024  aomclem8  43036  onsucf1o  43247  relexp0eq  43676  sprsymrelf1  47441  fmtnof1  47480  fmtnofac1  47515  prmdvdsfmtnof1  47532  sfprmdvdsmersenne  47548  gpgedgvtx0  47977  isupwlk  48010  uspgrsprf1  48021  2zlidl  48114  rrx2xpref1o  48597  rrx2plord  48599  rrx2plordisom  48602  sphere  48626  line2ylem  48630