Theorem eqeqan12d 2776

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2754

This theorem is used by:  eqeqan12rd  2777  eqeq12d  2778  eqeq12  2779  eqfnfv2  7027  f1mpt  7262  soisores  7332  xpopth  8031  f1o2ndf1  8123  fnwelem  8133  fnse  8135  tz7.48lem  8434  ecopoveq  8822  xpdom2  9074  unfilem2  9280  wemaplem1  9522  suc11reg  9602  oemapval  9666  cantnf  9676  wemapwe  9680  r0weon  10019  infxpen  10021  fodomacn  10063  sornom  10283  fin1a2lem2  10407  fin1a2lem4  10409  neg11  11537  subeqrev  11664  rpnnen1lem6  13036  cnref1o  13039  xneg11  13271  injresinj  13851  modadd1  13973  modaddid  13975  modmul1  13992  modlteq  14013  sq11  14199  hashen  14415  fz1eqb  14422  eqwrd  14626  s111  14687  ccatopth  14789  wrd2ind  14796  wwlktovf1  15034  cj11  15253  sqrt11  15353  sqabs  15398  recan  15428  reeff1  16214  efieq  16257  eulerthlem2  16879  vdwlem12  17090  xpsff1o  17659  ismgmhm  18804  ismhm  18899  isghm  19349  gsmsymgreq  19565  symgfixf1  19570  odf1  19695  sylow1  19736  frgpuplem  19905  rhmval0  20622  isdomn  20873  rngqiprngimfo  21510  pzriprnglem11  21710  cygznlem3  21788  psgnghm  21799  tgtop11  23213  fclsval  24240  vitali  25847  recosf1o  26780  mpodvdsmulf1o  27438  dvdsmulf1o  27440  fsumvma  27457  negs11  28322  oniso  28544  bdayn0sf1o  28643  brcgr  29365  axlowdimlem15  29421  axcontlem1  29429  axcontlem4  29432  axcontlem7  29435  axcontlem8  29436  iswlk  30078  wlkswwlksf1o  30355  wwlksnextinj  30375  clwlkclwwlkf1  30488  clwwlkf1  30527  numclwwlkqhash  30863  grpoinvf  31021  hial2eq2  31596  qusker  33797  bnj554  35416  erdszelem9  35786  sategoelfvb  36006  mrsubff1  36101  msubff1  36143  mvhf1  36146  fneval  36979  topfneec2  36983  bj-imdirval3  37944  f1omptsnlem  38098  f1omptsn  38099  rdgeqoa  38132  poimirlem4  38381  poimirlem26  38403  poimirlem27  38404  ismtyval  38558  extep  39045  brsucmap  39222  brdmqss  39486  disjimeceqim2  39561  qmapeldisjsim  39616  fimgmcyc  43424  sn-isghm  43527  wepwsolem  43891  fnwe2val  43898  aomclem8  43910  onsucf1o  44121  relexp0eq  44549  sprsymrelf1  48404  fmtnof1  48446  fmtnofac1  48481  prmdvdsfmtnof1  48498  sfprmdvdsmersenne  48514  gpgedgvtx0  48985  isupwlk  49060  uspgrsprf1  49071  2zlidl  49163  rrx2xpref1o  49656  rrx2plord  49658  rrx2plordisom  49661  sphere  49685  line2ylem  49689