Theorem eqeqan12d 2752

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1539

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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2730

This theorem is referenced by:  eqeqan12rd  2753  eqeq12d  2754  eqeq12  2755  eqfnfv2  6910  f1mpt  7134  soisores  7198  xpopth  7872  f1o2ndf1  7963  fnwelem  7972  fnse  7974  tz7.48lem  8272  ecopoveq  8607  xpdom2  8854  unfilem2  9079  wemaplem1  9305  suc11reg  9377  oemapval  9441  cantnf  9451  wemapwe  9455  r0weon  9768  infxpen  9770  fodomacn  9812  sornom  10033  fin1a2lem2  10157  fin1a2lem4  10159  neg11  11272  subeqrev  11397  rpnnen1lem6  12722  cnref1o  12725  xneg11  12949  injresinj  13508  modadd1  13628  modmul1  13644  modlteq  13665  sq11  13850  hashen  14061  fz1eqb  14069  eqwrd  14260  s111  14320  ccatopth  14429  wrd2ind  14436  wwlktovf1  14672  cj11  14873  sqrt11  14974  sqabs  15019  recan  15048  reeff1  15829  efieq  15872  eulerthlem2  16483  vdwlem12  16693  xpsff1o  17278  ismhm  18432  gsmsymgreq  19040  symgfixf1  19045  odf1  19169  sylow1  19208  frgpuplem  19378  isdomn  20565  cygznlem3  20777  psgnghm  20785  tgtop11  22132  fclsval  23159  vitali  24777  recosf1o  25691  dvdsmulf1o  26343  fsumvma  26361  brcgr  27268  axlowdimlem15  27324  axcontlem1  27332  axcontlem4  27335  axcontlem7  27338  axcontlem8  27339  iswlk  27977  wlkswwlksf1o  28244  wwlksnextinj  28264  clwlkclwwlkf1  28374  clwwlkf1  28413  numclwwlkqhash  28739  grpoinvf  28894  hial2eq2  29469  qusker  31549  bnj554  32879  erdszelem9  33161  sategoelfvb  33381  mrsubff1  33476  msubff1  33518  mvhf1  33521  fneval  34541  topfneec2  34545  bj-imdirval3  35355  f1omptsnlem  35507  f1omptsn  35508  rdgeqoa  35541  poimirlem4  35781  poimirlem26  35803  poimirlem27  35804  ismtyval  35958  extep  36418  brdmqss  36759  wepwsolem  40867  fnwe2val  40874  aomclem8  40886  relexp0eq  41309  sprsymrelf1  44948  fmtnof1  44987  fmtnofac1  45022  prmdvdsfmtnof1  45039  sfprmdvdsmersenne  45055  isupwlk  45298  uspgrsprf1  45309  ismgmhm  45337  2zlidl  45492  rrx2xpref1o  46064  rrx2plord  46066  rrx2plordisom  46069  sphere  46093  line2ylem  46097