Theorem eqeqan12d 2746

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

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

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724

This theorem is referenced by:  eqeqan12rd  2747  eqeq12d  2748  eqeq12  2749  eqfnfv2  7033  f1mpt  7259  soisores  7323  xpopth  8015  f1o2ndf1  8107  fnwelem  8116  fnse  8118  tz7.48lem  8440  ecopoveq  8811  xpdom2  9066  unfilem2  9310  wemaplem1  9540  suc11reg  9613  oemapval  9677  cantnf  9687  wemapwe  9691  r0weon  10006  infxpen  10008  fodomacn  10050  sornom  10271  fin1a2lem2  10395  fin1a2lem4  10397  neg11  11510  subeqrev  11635  rpnnen1lem6  12965  cnref1o  12968  xneg11  13193  injresinj  13752  modadd1  13872  modmul1  13888  modlteq  13909  sq11  14095  hashen  14306  fz1eqb  14313  eqwrd  14506  s111  14564  ccatopth  14665  wrd2ind  14672  wwlktovf1  14907  cj11  15108  sqrt11  15208  sqabs  15253  recan  15282  reeff1  16062  efieq  16105  eulerthlem2  16714  vdwlem12  16924  xpsff1o  17512  ismhm  18672  gsmsymgreq  19299  symgfixf1  19304  odf1  19429  sylow1  19470  frgpuplem  19639  isdomn  20909  cygznlem3  21124  psgnghm  21132  tgtop11  22484  fclsval  23511  vitali  25129  recosf1o  26043  dvdsmulf1o  26695  fsumvma  26713  negs11  27520  brcgr  28155  axlowdimlem15  28211  axcontlem1  28219  axcontlem4  28222  axcontlem7  28225  axcontlem8  28226  iswlk  28864  wlkswwlksf1o  29130  wwlksnextinj  29150  clwlkclwwlkf1  29260  clwwlkf1  29299  numclwwlkqhash  29625  grpoinvf  29780  hial2eq2  30355  qusker  32459  bnj554  33905  erdszelem9  34185  sategoelfvb  34405  mrsubff1  34500  msubff1  34542  mvhf1  34545  fneval  35232  topfneec2  35236  bj-imdirval3  36060  f1omptsnlem  36212  f1omptsn  36213  rdgeqoa  36246  poimirlem4  36487  poimirlem26  36509  poimirlem27  36510  ismtyval  36663  extep  37146  brdmqss  37511  wepwsolem  41774  fnwe2val  41781  aomclem8  41793  onsucf1o  42012  relexp0eq  42442  sprsymrelf1  46154  fmtnof1  46193  fmtnofac1  46228  prmdvdsfmtnof1  46245  sfprmdvdsmersenne  46261  isupwlk  46504  uspgrsprf1  46515  ismgmhm  46543  rngqiprngimfo  46776  pzriprnglem11  46805  2zlidl  46822  rrx2xpref1o  47394  rrx2plord  47396  rrx2plordisom  47399  sphere  47423  line2ylem  47427