Theorem eqeqan12d 2780

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2758

This theorem is used by:  eqeqan12rd  2781  eqeq12d  2782  eqeq12  2783  eqfnfv2  7033  f1mpt  7266  soisores  7336  xpopth  8036  f1o2ndf1  8126  fnwelem  8136  fnse  8138  tz7.48lem  8437  ecopoveq  8825  xpdom2  9070  unfilem2  9276  wemaplem1  9518  suc11reg  9598  oemapval  9662  cantnf  9672  wemapwe  9676  r0weon  10015  infxpen  10017  fodomacn  10059  sornom  10279  fin1a2lem2  10403  fin1a2lem4  10405  neg11  11527  subeqrev  11654  rpnnen1lem6  13024  cnref1o  13027  xneg11  13259  injresinj  13839  modadd1  13961  modaddid  13963  modmul1  13980  modlteq  14001  sq11  14187  hashen  14403  fz1eqb  14410  eqwrd  14614  s111  14675  ccatopth  14777  wrd2ind  14784  wwlktovf1  15020  cj11  15239  sqrt11  15339  sqabs  15384  recan  15414  reeff1  16201  efieq  16244  eulerthlem2  16866  vdwlem12  17077  xpsff1o  17646  ismgmhm  18783  ismhm  18874  isghm  19317  gsmsymgreq  19533  symgfixf1  19538  odf1  19663  sylow1  19704  frgpuplem  19873  rhmval0  20590  isdomn  20841  rngqiprngimfo  21478  pzriprnglem11  21678  cygznlem3  21756  psgnghm  21767  tgtop11  23176  fclsval  24202  vitali  25809  recosf1o  26737  mpodvdsmulf1o  27395  dvdsmulf1o  27397  fsumvma  27414  negs11  28279  oniso  28501  bdayn0sf1o  28600  brcgr  29287  axlowdimlem15  29343  axcontlem1  29351  axcontlem4  29354  axcontlem7  29357  axcontlem8  29358  iswlk  29997  wlkswwlksf1o  30265  wwlksnextinj  30285  clwlkclwwlkf1  30398  clwwlkf1  30437  numclwwlkqhash  30763  grpoinvf  30921  hial2eq2  31496  qusker  33700  bnj554  35319  erdszelem9  35712  sategoelfvb  35932  mrsubff1  36027  msubff1  36069  mvhf1  36072  fneval  36904  topfneec2  36908  bj-imdirval3  37869  f1omptsnlem  38023  f1omptsn  38024  rdgeqoa  38057  poimirlem4  38316  poimirlem26  38338  poimirlem27  38339  ismtyval  38492  extep  38979  brsucmap  39156  brdmqss  39420  disjimeceqim2  39495  qmapeldisjsim  39550  fimgmcyc  43343  sn-isghm  43446  wepwsolem  43810  fnwe2val  43817  aomclem8  43829  onsucf1o  44040  relexp0eq  44468  sprsymrelf1  48286  fmtnof1  48328  fmtnofac1  48363  prmdvdsfmtnof1  48380  sfprmdvdsmersenne  48396  gpgedgvtx0  48867  isupwlk  48942  uspgrsprf1  48953  2zlidl  49046  rrx2xpref1o  49539  rrx2plord  49541  rrx2plordisom  49544  sphere  49568  line2ylem  49572