Theorem eqeqan12d 2775

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   = wceq 1559

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753

This theorem is referenced by:  eqeqan12rd  2776  eqeq12d  2777  eqeq12  2778  eqfnfv2  7008  f1mpt  7241  soisores  7307  xpopth  8007  f1o2ndf1  8096  fnwelem  8106  fnse  8108  tz7.48lem  8407  ecopoveq  8795  xpdom2  9040  unfilem2  9246  wemaplem1  9491  suc11reg  9571  oemapval  9635  cantnf  9645  wemapwe  9649  r0weon  9965  infxpen  9967  fodomacn  10009  sornom  10231  fin1a2lem2  10355  fin1a2lem4  10357  neg11  11479  subeqrev  11606  rpnnen1lem6  12980  cnref1o  12983  xneg11  13215  injresinj  13794  modadd1  13915  modaddid  13917  modmul1  13934  modlteq  13955  sq11  14141  hashen  14357  fz1eqb  14364  eqwrd  14567  s111  14626  ccatopth  14726  wrd2ind  14733  wwlktovf1  14967  cj11  15172  sqrt11  15272  sqabs  15317  recan  15347  reeff1  16135  efieq  16178  eulerthlem2  16800  vdwlem12  17011  xpsff1o  17580  ismgmhm  18713  ismhm  18802  isghm  19239  gsmsymgreq  19455  symgfixf1  19460  odf1  19585  sylow1  19626  frgpuplem  19795  isdomn  20734  rngqiprngimfo  21351  pzriprnglem11  21523  cygznlem3  21601  psgnghm  21612  tgtop11  23022  fclsval  24048  vitali  25655  recosf1o  26577  mpodvdsmulf1o  27235  dvdsmulf1o  27237  fsumvma  27254  negs11  28119  oniso  28341  bdayn0sf1o  28440  brcgr  29047  axlowdimlem15  29103  axcontlem1  29111  axcontlem4  29114  axcontlem7  29117  axcontlem8  29118  iswlk  29757  wlkswwlksf1o  30025  wwlksnextinj  30045  clwlkclwwlkf1  30158  clwwlkf1  30197  numclwwlkqhash  30523  grpoinvf  30681  hial2eq2  31256  qusker  33496  bnj554  35158  erdszelem9  35513  sategoelfvb  35733  mrsubff1  35828  msubff1  35870  mvhf1  35873  fneval  36676  topfneec2  36680  bj-imdirval3  37640  f1omptsnlem  37794  f1omptsn  37795  rdgeqoa  37828  poimirlem4  38087  poimirlem26  38109  poimirlem27  38110  ismtyval  38263  extep  38752  brsucmap  38929  brdmqss  39193  disjimeceqim2  39268  qmapeldisjsim  39323  fimgmcyc  43116  sn-isghm  43219  wepwsolem  43583  fnwe2val  43590  aomclem8  43602  onsucf1o  43813  relexp0eq  44241  sprsymrelf1  48066  fmtnof1  48108  fmtnofac1  48143  prmdvdsfmtnof1  48160  sfprmdvdsmersenne  48176  gpgedgvtx0  48647  isupwlk  48722  uspgrsprf1  48733  2zlidl  48826  rrx2xpref1o  49304  rrx2plord  49306  rrx2plordisom  49309  sphere  49333  line2ylem  49337