Theorem eqeqan12d 2743

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721

This theorem is referenced by:  eqeqan12rd  2744  eqeq12d  2745  eqeq12  2746  eqfnfv2  6970  f1mpt  7202  soisores  7268  xpopth  7972  f1o2ndf1  8062  fnwelem  8071  fnse  8073  tz7.48lem  8370  ecopoveq  8752  xpdom2  8996  unfilem2  9213  wemaplem1  9457  suc11reg  9534  oemapval  9598  cantnf  9608  wemapwe  9612  r0weon  9925  infxpen  9927  fodomacn  9969  sornom  10190  fin1a2lem2  10314  fin1a2lem4  10316  neg11  11433  subeqrev  11560  rpnnen1lem6  12901  cnref1o  12904  xneg11  13135  injresinj  13709  modadd1  13830  modaddid  13832  modmul1  13849  modlteq  13870  sq11  14056  hashen  14272  fz1eqb  14279  eqwrd  14482  s111  14540  ccatopth  14640  wrd2ind  14647  wwlktovf1  14882  cj11  15087  sqrt11  15187  sqabs  15232  recan  15262  reeff1  16047  efieq  16090  eulerthlem2  16711  vdwlem12  16922  xpsff1o  17489  ismgmhm  18588  ismhm  18677  isghm  19112  gsmsymgreq  19329  symgfixf1  19334  odf1  19459  sylow1  19500  frgpuplem  19669  isdomn  20608  rngqiprngimfo  21226  pzriprnglem11  21416  cygznlem3  21494  psgnghm  21505  tgtop11  22885  fclsval  23911  vitali  25530  recosf1o  26460  mpodvdsmulf1o  27120  dvdsmulf1o  27122  fsumvma  27140  negs11  27978  onsiso  28192  bdayn0sf1o  28282  brcgr  28863  axlowdimlem15  28919  axcontlem1  28927  axcontlem4  28930  axcontlem7  28933  axcontlem8  28934  iswlk  29574  wlkswwlksf1o  29842  wwlksnextinj  29862  clwlkclwwlkf1  29972  clwwlkf1  30011  numclwwlkqhash  30337  grpoinvf  30494  hial2eq2  31069  qusker  33299  bnj554  34868  erdszelem9  35174  sategoelfvb  35394  mrsubff1  35489  msubff1  35531  mvhf1  35534  fneval  36328  topfneec2  36332  bj-imdirval3  37160  f1omptsnlem  37312  f1omptsn  37313  rdgeqoa  37346  poimirlem4  37606  poimirlem26  37628  poimirlem27  37629  ismtyval  37782  extep  38259  brdmqss  38625  fimgmcyc  42510  sn-isghm  42649  wepwsolem  43018  fnwe2val  43025  aomclem8  43037  onsucf1o  43248  relexp0eq  43677  sprsymrelf1  47484  fmtnof1  47523  fmtnofac1  47558  prmdvdsfmtnof1  47575  sfprmdvdsmersenne  47591  gpgedgvtx0  48049  isupwlk  48124  uspgrsprf1  48135  2zlidl  48228  rrx2xpref1o  48707  rrx2plord  48709  rrx2plordisom  48712  sphere  48736  line2ylem  48740