Theorem eqeqan12d 2777

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1570

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755

This theorem is referenced by:  eqeqan12rd  2778  eqeq12d  2779  eqeq12  2780  eqfnfv2  7028  f1mpt  7261  soisores  7327  xpopth  8028  f1o2ndf1  8118  fnwelem  8128  fnse  8130  tz7.48lem  8429  ecopoveq  8817  xpdom2  9061  unfilem2  9267  wemaplem1  9509  suc11reg  9589  oemapval  9653  cantnf  9663  wemapwe  9667  r0weon  9997  infxpen  9999  fodomacn  10041  sornom  10262  fin1a2lem2  10386  fin1a2lem4  10388  neg11  11510  subeqrev  11637  rpnnen1lem6  13007  cnref1o  13010  xneg11  13242  injresinj  13822  modadd1  13943  modaddid  13945  modmul1  13962  modlteq  13983  sq11  14169  hashen  14385  fz1eqb  14392  eqwrd  14596  s111  14655  ccatopth  14755  wrd2ind  14762  wwlktovf1  14996  cj11  15215  sqrt11  15315  sqabs  15360  recan  15390  reeff1  16177  efieq  16220  eulerthlem2  16842  vdwlem12  17053  xpsff1o  17622  ismgmhm  18755  ismhm  18844  isghm  19287  gsmsymgreq  19503  symgfixf1  19508  odf1  19633  sylow1  19674  frgpuplem  19843  isdomn  20791  rngqiprngimfo  21422  pzriprnglem11  21622  cygznlem3  21700  psgnghm  21711  tgtop11  23120  fclsval  24146  vitali  25753  recosf1o  26681  mpodvdsmulf1o  27339  dvdsmulf1o  27341  fsumvma  27358  negs11  28223  oniso  28445  bdayn0sf1o  28544  brcgr  29231  axlowdimlem15  29287  axcontlem1  29295  axcontlem4  29298  axcontlem7  29301  axcontlem8  29302  iswlk  29941  wlkswwlksf1o  30209  wwlksnextinj  30229  clwlkclwwlkf1  30342  clwwlkf1  30381  numclwwlkqhash  30707  grpoinvf  30865  hial2eq2  31440  qusker  33650  bnj554  35268  erdszelem9  35672  sategoelfvb  35892  mrsubff1  35987  msubff1  36029  mvhf1  36032  fneval  36844  topfneec2  36848  bj-imdirval3  37809  f1omptsnlem  37963  f1omptsn  37964  rdgeqoa  37997  poimirlem4  38256  poimirlem26  38278  poimirlem27  38279  ismtyval  38432  extep  38919  brsucmap  39096  brdmqss  39360  disjimeceqim2  39435  qmapeldisjsim  39490  fimgmcyc  43285  sn-isghm  43388  wepwsolem  43752  fnwe2val  43759  aomclem8  43771  onsucf1o  43982  relexp0eq  44410  sprsymrelf1  48228  fmtnof1  48270  fmtnofac1  48305  prmdvdsfmtnof1  48322  sfprmdvdsmersenne  48338  gpgedgvtx0  48809  isupwlk  48884  uspgrsprf1  48895  2zlidl  48988  rrx2xpref1o  49481  rrx2plord  49483  rrx2plordisom  49486  sphere  49510  line2ylem  49514