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  7004  f1mpt  7236  soisores  7302  xpopth  8009  f1o2ndf1  8101  fnwelem  8110  fnse  8112  tz7.48lem  8409  ecopoveq  8791  xpdom2  9036  unfilem2  9255  wemaplem1  9499  suc11reg  9572  oemapval  9636  cantnf  9646  wemapwe  9650  r0weon  9965  infxpen  9967  fodomacn  10009  sornom  10230  fin1a2lem2  10354  fin1a2lem4  10356  neg11  11473  subeqrev  11600  rpnnen1lem6  12941  cnref1o  12944  xneg11  13175  injresinj  13749  modadd1  13870  modaddid  13872  modmul1  13889  modlteq  13910  sq11  14096  hashen  14312  fz1eqb  14319  eqwrd  14522  s111  14580  ccatopth  14681  wrd2ind  14688  wwlktovf1  14923  cj11  15128  sqrt11  15228  sqabs  15273  recan  15303  reeff1  16088  efieq  16131  eulerthlem2  16752  vdwlem12  16963  xpsff1o  17530  ismgmhm  18623  ismhm  18712  isghm  19147  gsmsymgreq  19362  symgfixf1  19367  odf1  19492  sylow1  19533  frgpuplem  19702  isdomn  20614  rngqiprngimfo  21211  pzriprnglem11  21401  cygznlem3  21479  psgnghm  21489  tgtop11  22869  fclsval  23895  vitali  25514  recosf1o  26444  mpodvdsmulf1o  27104  dvdsmulf1o  27106  fsumvma  27124  negs11  27955  onsiso  28169  bdayn0sf1o  28259  brcgr  28827  axlowdimlem15  28883  axcontlem1  28891  axcontlem4  28894  axcontlem7  28897  axcontlem8  28898  iswlk  29538  wlkswwlksf1o  29809  wwlksnextinj  29829  clwlkclwwlkf1  29939  clwwlkf1  29978  numclwwlkqhash  30304  grpoinvf  30461  hial2eq2  31036  qusker  33320  bnj554  34889  erdszelem9  35186  sategoelfvb  35406  mrsubff1  35501  msubff1  35543  mvhf1  35546  fneval  36340  topfneec2  36344  bj-imdirval3  37172  f1omptsnlem  37324  f1omptsn  37325  rdgeqoa  37358  poimirlem4  37618  poimirlem26  37640  poimirlem27  37641  ismtyval  37794  extep  38271  brdmqss  38637  fimgmcyc  42522  sn-isghm  42661  wepwsolem  43031  fnwe2val  43038  aomclem8  43050  onsucf1o  43261  relexp0eq  43690  sprsymrelf1  47497  fmtnof1  47536  fmtnofac1  47571  prmdvdsfmtnof1  47588  sfprmdvdsmersenne  47604  gpgedgvtx0  48052  isupwlk  48124  uspgrsprf1  48135  2zlidl  48228  rrx2xpref1o  48707  rrx2plord  48709  rrx2plordisom  48712  sphere  48736  line2ylem  48740