Theorem eqeqan12d 2742

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   = wceq 1533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-9 2108  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-cleq 2720

This theorem is referenced by:  eqeqan12rd  2743  eqeq12d  2744  eqeq12  2745  eqfnfv2  7046  f1mpt  7277  soisores  7341  xpopth  8040  f1o2ndf1  8133  fnwelem  8142  fnse  8144  tz7.48lem  8468  ecopoveq  8843  xpdom2  9098  unfilem2  9342  wemaplem1  9577  suc11reg  9650  oemapval  9714  cantnf  9724  wemapwe  9728  r0weon  10043  infxpen  10045  fodomacn  10087  sornom  10308  fin1a2lem2  10432  fin1a2lem4  10434  neg11  11549  subeqrev  11674  rpnnen1lem6  13004  cnref1o  13007  xneg11  13234  injresinj  13793  modadd1  13913  modmul1  13929  modlteq  13950  sq11  14135  hashen  14346  fz1eqb  14353  eqwrd  14547  s111  14605  ccatopth  14706  wrd2ind  14713  wwlktovf1  14948  cj11  15149  sqrt11  15249  sqabs  15294  recan  15323  reeff1  16104  efieq  16147  eulerthlem2  16758  vdwlem12  16968  xpsff1o  17556  ismgmhm  18663  ismhm  18749  gsmsymgreq  19394  symgfixf1  19399  odf1  19524  sylow1  19565  frgpuplem  19734  rngqiprngimfo  21198  isdomn  21248  pzriprnglem11  21424  cygznlem3  21510  psgnghm  21519  tgtop11  22905  fclsval  23932  vitali  25562  recosf1o  26489  mpodvdsmulf1o  27146  dvdsmulf1o  27148  fsumvma  27166  negs11  27981  brcgr  28731  axlowdimlem15  28787  axcontlem1  28795  axcontlem4  28798  axcontlem7  28801  axcontlem8  28802  iswlk  29444  wlkswwlksf1o  29710  wwlksnextinj  29730  clwlkclwwlkf1  29840  clwwlkf1  29879  numclwwlkqhash  30205  grpoinvf  30362  hial2eq2  30937  qusker  33085  bnj554  34563  erdszelem9  34842  sategoelfvb  35062  mrsubff1  35157  msubff1  35199  mvhf1  35202  fneval  35869  topfneec2  35873  bj-imdirval3  36696  f1omptsnlem  36848  f1omptsn  36849  rdgeqoa  36882  poimirlem4  37130  poimirlem26  37152  poimirlem27  37153  ismtyval  37306  extep  37787  brdmqss  38150  wepwsolem  42497  fnwe2val  42504  aomclem8  42516  onsucf1o  42732  relexp0eq  43162  sprsymrelf1  46865  fmtnof1  46904  fmtnofac1  46939  prmdvdsfmtnof1  46956  sfprmdvdsmersenne  46972  isupwlk  47276  uspgrsprf1  47287  2zlidl  47380  rrx2xpref1o  47869  rrx2plord  47871  rrx2plordisom  47874  sphere  47898  line2ylem  47902