Theorem eqeqan12d 2751

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

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

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729

This theorem is referenced by:  eqeqan12rd  2752  eqeq12d  2753  eqeq12  2754  eqfnfv2  6978  f1mpt  7209  soisores  7275  xpopth  7976  f1o2ndf1  8065  fnwelem  8074  fnse  8076  tz7.48lem  8373  ecopoveq  8758  xpdom2  9003  unfilem2  9209  wemaplem1  9454  suc11reg  9531  oemapval  9595  cantnf  9605  wemapwe  9609  r0weon  9925  infxpen  9927  fodomacn  9969  sornom  10190  fin1a2lem2  10314  fin1a2lem4  10316  neg11  11436  subeqrev  11563  rpnnen1lem6  12923  cnref1o  12926  xneg11  13158  injresinj  13737  modadd1  13858  modaddid  13860  modmul1  13877  modlteq  13898  sq11  14084  hashen  14300  fz1eqb  14307  eqwrd  14510  s111  14569  ccatopth  14669  wrd2ind  14676  wwlktovf1  14910  cj11  15115  sqrt11  15215  sqabs  15260  recan  15290  reeff1  16078  efieq  16121  eulerthlem2  16743  vdwlem12  16954  xpsff1o  17522  ismgmhm  18655  ismhm  18744  isghm  19181  gsmsymgreq  19398  symgfixf1  19403  odf1  19528  sylow1  19569  frgpuplem  19738  isdomn  20673  rngqiprngimfo  21291  pzriprnglem11  21481  cygznlem3  21559  psgnghm  21570  tgtop11  22957  fclsval  23983  vitali  25590  recosf1o  26512  mpodvdsmulf1o  27171  dvdsmulf1o  27173  fsumvma  27190  negs11  28055  oniso  28277  bdayn0sf1o  28376  brcgr  28983  axlowdimlem15  29039  axcontlem1  29047  axcontlem4  29050  axcontlem7  29053  axcontlem8  29054  iswlk  29694  wlkswwlksf1o  29962  wwlksnextinj  29982  clwlkclwwlkf1  30095  clwwlkf1  30134  numclwwlkqhash  30460  grpoinvf  30618  hial2eq2  31193  qusker  33424  bnj554  35057  erdszelem9  35397  sategoelfvb  35617  mrsubff1  35712  msubff1  35754  mvhf1  35757  fneval  36550  topfneec2  36554  bj-imdirval3  37514  f1omptsnlem  37666  f1omptsn  37667  rdgeqoa  37700  poimirlem4  37959  poimirlem26  37981  poimirlem27  37982  ismtyval  38135  extep  38624  brsucmap  38801  brdmqss  39065  disjimeceqim2  39140  qmapeldisjsim  39195  fimgmcyc  42993  sn-isghm  43120  wepwsolem  43488  fnwe2val  43495  aomclem8  43507  onsucf1o  43718  relexp0eq  44146  sprsymrelf1  47968  fmtnof1  48010  fmtnofac1  48045  prmdvdsfmtnof1  48062  sfprmdvdsmersenne  48078  gpgedgvtx0  48549  isupwlk  48624  uspgrsprf1  48635  2zlidl  48728  rrx2xpref1o  49206  rrx2plord  49208  rrx2plordisom  49211  sphere  49235  line2ylem  49239