Theorem eqeqan12d 2774

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752

This theorem is used by:  eqeqan12rd  2775  eqeq12d  2776  eqeq12  2777  eqfnfv2  7030  f1mpt  7265  soisores  7335  xpopth  8042  f1o2ndf1  8135  fnwelem  8145  fnwe2lem1  8147  fnse  8152  onelfvnef1  8452  tz7.48lem  8453  tz7.48lemOLD  8454  ecopoveq  8842  xpdom2  9094  unfilem2  9301  wemaplem1  9543  suc11reg  9623  oemapval  9687  cantnf  9697  wemapwe  9701  r0weon  10094  infxpen  10096  fodomacn  10138  sornom  10358  fin1a2lem2  10482  fin1a2lem4  10484  neg11  11612  subeqrev  11741  rpnnen1lem6  13113  cnref1o  13116  xneg11  13348  injresinj  13929  modadd1  14051  modaddid  14053  modmul1  14070  modlteq  14091  sq11  14277  hashen  14494  fz1eqb  14501  eqwrd  14705  s111  14767  ccatopth  14869  wrd2ind  14876  wwlktovf1  15115  cj11  15334  sqrt11  15434  sqabs  15479  recan  15509  reeff1  16293  efieq  16336  eulerthlem2  16964  vdwlem12  17175  xpsff1o  17744  ismgmhm  18890  ismhm  18985  isghm  19435  gsmsymgreq  19651  symgfixf1  19656  odf1  19781  sylow1  19822  frgpuplem  19991  rhmval0  20710  isdomn  20962  rngqiprngimfo  21602  pzriprnglem11  21802  cygznlem3  21880  psgnghm  21891  tgtop11  23305  fclsval  24332  vitali  25939  recosf1o  26868  mpodvdsmulf1o  27526  dvdsmulf1o  27528  fsumvma  27545  negs11  28440  oniso  28662  bdayn0sf1o  28761  brcgr  29483  axlowdimlem15  29539  axcontlem1  29547  axcontlem4  29550  axcontlem7  29553  axcontlem8  29554  iswlk  30196  wlkswwlksf1o  30473  wwlksnextinj  30493  clwlkclwwlkf1  30606  clwwlkf1  30645  numclwwlkqhash  30981  grpoinvf  31139  hial2eq2  31714  qusker  33956  bnj554  35575  jaeqifi  35758  erdszelem9  36050  sategoelfvb  36270  mrsubff1  36365  msubff1  36407  mvhf1  36410  fneval  37232  topfneec2  37236  bj-imdirval3  38198  f1omptsnlem  38352  f1omptsn  38353  rdgeqoa  38386  poimirlem4  38635  poimirlem26  38657  poimirlem27  38658  ismtyval  38827  extep  39314  brsucmap  39491  brdmqss  39755  disjimeceqim2  39830  qmapeldisjsim  39885  fimgmcyc  43691  sn-isghm  43777  wepwsolem  44142  aomclem8  44156  onsucf1o  44367  relexp0eq  44794  sprsymrelf1  48671  fmtnof1  48713  fmtnofac1  48748  prmdvdsfmtnof1  48765  sfprmdvdsmersenne  48781  gpgedgvtx0  49252  isupwlk  49327  uspgrsprf1  49338  2zlidl  49430  rrx2plord  49926  rrx2plordisom  49929  sphere  49952  line2ylem  49956