Theorem eqeqan12d 2667

Description: A useful inference for substituting definitions into an equality. See also eqeqan12dALT 2668. (Contributed by NM, 9-Aug-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 20-Nov-2019.)

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	adantr 480	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐵)
3		eqeqan12d.2	. . 3 ⊢ (𝜓 → 𝐶 = 𝐷)
4	3	adantl 481	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝐶 = 𝐷)
5	2, 4	eqeq12d 2666	1 ⊢ ((𝜑 ∧ 𝜓) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1523

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644

This theorem is referenced by:  eqeqan12rd  2669  eqfnfv2  6352  f1mpt  6558  soisores  6617  xpopth  7251  f1o2ndf1  7330  fnwelem  7337  fnse  7339  tz7.48lem  7581  ecopoveq  7891  xpdom2  8096  unfilem2  8266  wemaplem1  8492  suc11reg  8554  oemapval  8618  cantnf  8628  wemapwe  8632  r0weon  8873  infxpen  8875  fodomacn  8917  sornom  9137  fin1a2lem2  9261  fin1a2lem4  9263  neg11  10370  subeqrev  10491  rpnnen1lem6  11857  rpnnen1OLD  11863  cnref1o  11865  xneg11  12084  injresinj  12629  modadd1  12747  modmul1  12763  modlteq  12784  sq11  12976  hashen  13175  fz1eqb  13183  eqwrd  13379  s111  13432  wrd2ind  13523  wwlktovf1  13746  cj11  13946  sqrt11  14047  sqabs  14091  recan  14120  reeff1  14894  efieq  14937  eulerthlem2  15534  vdwlem12  15743  xpsff1o  16275  ismhm  17384  gsmsymgreq  17898  symgfixf1  17903  odf1  18025  sylow1  18064  frgpuplem  18231  isdomn  19342  cygznlem3  19966  psgnghm  19974  tgtop11  20834  fclsval  21859  vitali  23427  recosf1o  24326  dvdsmulf1o  24965  fsumvma  24983  brcgr  25825  axlowdimlem15  25881  axcontlem1  25889  axcontlem4  25892  axcontlem7  25895  axcontlem8  25896  iswlk  26562  wlkpwwlkf1ouspgr  26833  wlknwwlksninj  26843  wlkwwlkinj  26850  wwlksnextinj  26862  clwwlkf1  27012  numclwwlkqhash  27355  grpoinvf  27514  hial2eq2  28092  bnj554  31095  erdszelem9  31307  mrsubff1  31537  msubff1  31579  mvhf1  31582  fneval  32472  topfneec2  32476  f1omptsnlem  33313  f1omptsn  33314  rdgeqoa  33348  poimirlem4  33543  poimirlem26  33565  poimirlem27  33566  ismtyval  33729  extep  34189  wepwsolem  37929  fnwe2val  37936  aomclem8  37948  relexp0eq  38310  fmtnof1  41772  fmtnofac1  41807  prmdvdsfmtnof1  41824  sfprmdvdsmersenne  41845  isupwlk  42042  sprsymrelf1  42071  uspgrsprf1  42080  ismgmhm  42108  2zlidl  42259