Theorem eqeqan12d 2747

Description: A useful inference for substituting definitions into an equality. See also eqeqan12dALT 2752. (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 509	1 ⊢ ((𝜑 ∧ 𝜓) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725

This theorem is referenced by:  eqeqan12rd  2748  eqeq12d  2749  eqeq12  2750  eqfnfv2  6973  f1mpt  7203  soisores  7269  xpopth  7970  f1o2ndf1  8060  fnwelem  8069  fnse  8071  tz7.48lem  8368  ecopoveq  8750  xpdom2  8994  unfilem2  9199  wemaplem1  9441  suc11reg  9518  oemapval  9582  cantnf  9592  wemapwe  9596  r0weon  9912  infxpen  9914  fodomacn  9956  sornom  10177  fin1a2lem2  10301  fin1a2lem4  10303  neg11  11421  subeqrev  11548  rpnnen1lem6  12884  cnref1o  12887  xneg11  13118  injresinj  13695  modadd1  13816  modaddid  13818  modmul1  13835  modlteq  13856  sq11  14042  hashen  14258  fz1eqb  14265  eqwrd  14468  s111  14527  ccatopth  14627  wrd2ind  14634  wwlktovf1  14868  cj11  15073  sqrt11  15173  sqabs  15218  recan  15248  reeff1  16033  efieq  16076  eulerthlem2  16697  vdwlem12  16908  xpsff1o  17475  ismgmhm  18608  ismhm  18697  isghm  19131  gsmsymgreq  19348  symgfixf1  19353  odf1  19478  sylow1  19519  frgpuplem  19688  isdomn  20624  rngqiprngimfo  21242  pzriprnglem11  21432  cygznlem3  21510  psgnghm  21521  tgtop11  22900  fclsval  23926  vitali  25544  recosf1o  26474  mpodvdsmulf1o  27134  dvdsmulf1o  27136  fsumvma  27154  negs11  27994  onsiso  28208  bdayn0sf1o  28298  brcgr  28882  axlowdimlem15  28938  axcontlem1  28946  axcontlem4  28949  axcontlem7  28952  axcontlem8  28953  iswlk  29593  wlkswwlksf1o  29861  wwlksnextinj  29881  clwlkclwwlkf1  29994  clwwlkf1  30033  numclwwlkqhash  30359  grpoinvf  30516  hial2eq2  31091  qusker  33323  bnj554  34934  erdszelem9  35266  sategoelfvb  35486  mrsubff1  35581  msubff1  35623  mvhf1  35626  fneval  36419  topfneec2  36423  bj-imdirval3  37251  f1omptsnlem  37403  f1omptsn  37404  rdgeqoa  37437  poimirlem4  37687  poimirlem26  37709  poimirlem27  37710  ismtyval  37863  extep  38344  brsucmap  38502  brdmqss  38766  fimgmcyc  42655  sn-isghm  42794  wepwsolem  43162  fnwe2val  43169  aomclem8  43181  onsucf1o  43392  relexp0eq  43821  sprsymrelf1  47623  fmtnof1  47662  fmtnofac1  47697  prmdvdsfmtnof1  47714  sfprmdvdsmersenne  47730  gpgedgvtx0  48188  isupwlk  48263  uspgrsprf1  48274  2zlidl  48367  rrx2xpref1o  48846  rrx2plord  48848  rrx2plordisom  48851  sphere  48875  line2ylem  48879