Theorem eqeqan12d 2746

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541

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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724

This theorem is referenced by:  eqeqan12rd  2747  eqeq12d  2748  eqeq12  2749  eqfnfv2  7033  f1mpt  7262  soisores  7326  xpopth  8018  f1o2ndf1  8110  fnwelem  8119  fnse  8121  tz7.48lem  8443  ecopoveq  8814  xpdom2  9069  unfilem2  9313  wemaplem1  9543  suc11reg  9616  oemapval  9680  cantnf  9690  wemapwe  9694  r0weon  10009  infxpen  10011  fodomacn  10053  sornom  10274  fin1a2lem2  10398  fin1a2lem4  10400  neg11  11513  subeqrev  11638  rpnnen1lem6  12968  cnref1o  12971  xneg11  13196  injresinj  13755  modadd1  13875  modmul1  13891  modlteq  13912  sq11  14098  hashen  14309  fz1eqb  14316  eqwrd  14509  s111  14567  ccatopth  14668  wrd2ind  14675  wwlktovf1  14910  cj11  15111  sqrt11  15211  sqabs  15256  recan  15285  reeff1  16065  efieq  16108  eulerthlem2  16717  vdwlem12  16927  xpsff1o  17515  ismhm  18675  gsmsymgreq  19302  symgfixf1  19307  odf1  19432  sylow1  19473  frgpuplem  19642  isdomn  20916  cygznlem3  21131  psgnghm  21139  tgtop11  22492  fclsval  23519  vitali  25137  recosf1o  26051  dvdsmulf1o  26705  fsumvma  26723  negs11  27533  brcgr  28196  axlowdimlem15  28252  axcontlem1  28260  axcontlem4  28263  axcontlem7  28266  axcontlem8  28267  iswlk  28905  wlkswwlksf1o  29171  wwlksnextinj  29191  clwlkclwwlkf1  29301  clwwlkf1  29340  numclwwlkqhash  29666  grpoinvf  29823  hial2eq2  30398  qusker  32505  bnj554  33979  erdszelem9  34259  sategoelfvb  34479  mrsubff1  34574  msubff1  34616  mvhf1  34619  fneval  35323  topfneec2  35327  bj-imdirval3  36151  f1omptsnlem  36303  f1omptsn  36304  rdgeqoa  36337  poimirlem4  36578  poimirlem26  36600  poimirlem27  36601  ismtyval  36754  extep  37237  brdmqss  37602  wepwsolem  41866  fnwe2val  41873  aomclem8  41885  onsucf1o  42104  relexp0eq  42534  sprsymrelf1  46243  fmtnof1  46282  fmtnofac1  46317  prmdvdsfmtnof1  46334  sfprmdvdsmersenne  46350  isupwlk  46593  uspgrsprf1  46604  ismgmhm  46632  rngqiprngimfo  46865  pzriprnglem11  46894  2zlidl  46911  rrx2xpref1o  47482  rrx2plord  47484  rrx2plordisom  47487  sphere  47511  line2ylem  47515