Theorem eqeqan12d 2779

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-cleq 2757

This theorem is referenced by:  eqeqan12rd  2780  eqeq12d  2781  eqeq12  2782  eqfnfv2  7016  f1mpt  7249  soisores  7315  xpopth  8015  f1o2ndf1  8105  fnwelem  8115  fnse  8117  tz7.48lem  8416  ecopoveq  8804  xpdom2  9048  unfilem2  9254  wemaplem1  9496  suc11reg  9576  oemapval  9640  cantnf  9650  wemapwe  9654  r0weon  9984  infxpen  9986  fodomacn  10028  sornom  10249  fin1a2lem2  10373  fin1a2lem4  10375  neg11  11497  subeqrev  11624  rpnnen1lem6  12994  cnref1o  12997  xneg11  13229  injresinj  13808  modadd1  13929  modaddid  13931  modmul1  13948  modlteq  13969  sq11  14155  hashen  14371  fz1eqb  14378  eqwrd  14582  s111  14641  ccatopth  14741  wrd2ind  14748  wwlktovf1  14982  cj11  15201  sqrt11  15301  sqabs  15346  recan  15376  reeff1  16164  efieq  16207  eulerthlem2  16829  vdwlem12  17040  xpsff1o  17609  ismgmhm  18742  ismhm  18831  isghm  19274  gsmsymgreq  19490  symgfixf1  19495  odf1  19620  sylow1  19661  frgpuplem  19830  isdomn  20778  rngqiprngimfo  21400  pzriprnglem11  21598  cygznlem3  21676  psgnghm  21687  tgtop11  23096  fclsval  24122  vitali  25729  recosf1o  26654  mpodvdsmulf1o  27312  dvdsmulf1o  27314  fsumvma  27331  negs11  28196  oniso  28418  bdayn0sf1o  28517  brcgr  29155  axlowdimlem15  29211  axcontlem1  29219  axcontlem4  29222  axcontlem7  29225  axcontlem8  29226  iswlk  29865  wlkswwlksf1o  30133  wwlksnextinj  30153  clwlkclwwlkf1  30266  clwwlkf1  30305  numclwwlkqhash  30631  grpoinvf  30789  hial2eq2  31364  qusker  33579  bnj554  35199  erdszelem9  35557  sategoelfvb  35777  mrsubff1  35872  msubff1  35914  mvhf1  35917  fneval  36720  topfneec2  36724  bj-imdirval3  37683  f1omptsnlem  37837  f1omptsn  37838  rdgeqoa  37871  poimirlem4  38130  poimirlem26  38152  poimirlem27  38153  ismtyval  38306  extep  38795  brsucmap  38972  brdmqss  39236  disjimeceqim2  39311  qmapeldisjsim  39366  fimgmcyc  43159  sn-isghm  43262  wepwsolem  43626  fnwe2val  43633  aomclem8  43645  onsucf1o  43856  relexp0eq  44284  sprsymrelf1  48101  fmtnof1  48143  fmtnofac1  48178  prmdvdsfmtnof1  48195  sfprmdvdsmersenne  48211  gpgedgvtx0  48682  isupwlk  48757  uspgrsprf1  48768  2zlidl  48861  rrx2xpref1o  49350  rrx2plord  49352  rrx2plordisom  49355  sphere  49379  line2ylem  49383