Theorem eqeqan12d 2748

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-cleq 2726

This theorem is referenced by:  eqeqan12rd  2749  eqeq12d  2750  eqeq12  2751  eqfnfv2  7033  f1mpt  7264  soisores  7330  xpopth  8038  f1o2ndf1  8130  fnwelem  8139  fnse  8141  tz7.48lem  8464  ecopoveq  8841  xpdom2  9090  unfilem2  9327  wemaplem1  9569  suc11reg  9642  oemapval  9706  cantnf  9716  wemapwe  9720  r0weon  10035  infxpen  10037  fodomacn  10079  sornom  10300  fin1a2lem2  10424  fin1a2lem4  10426  neg11  11543  subeqrev  11668  rpnnen1lem6  13007  cnref1o  13010  xneg11  13240  injresinj  13810  modadd1  13931  modmul1  13948  modlteq  13969  sq11  14154  hashen  14369  fz1eqb  14376  eqwrd  14578  s111  14636  ccatopth  14737  wrd2ind  14744  wwlktovf1  14979  cj11  15184  sqrt11  15284  sqabs  15329  recan  15358  reeff1  16139  efieq  16182  eulerthlem2  16802  vdwlem12  17013  xpsff1o  17588  ismgmhm  18683  ismhm  18772  isghm  19207  gsmsymgreq  19423  symgfixf1  19428  odf1  19553  sylow1  19594  frgpuplem  19763  isdomn  20678  rngqiprngimfo  21278  pzriprnglem11  21469  cygznlem3  21555  psgnghm  21565  tgtop11  22955  fclsval  23981  vitali  25603  recosf1o  26532  mpodvdsmulf1o  27192  dvdsmulf1o  27194  fsumvma  27212  negs11  28036  brcgr  28864  axlowdimlem15  28920  axcontlem1  28928  axcontlem4  28931  axcontlem7  28934  axcontlem8  28935  iswlk  29575  wlkswwlksf1o  29846  wwlksnextinj  29866  clwlkclwwlkf1  29976  clwwlkf1  30015  numclwwlkqhash  30341  grpoinvf  30498  hial2eq2  31073  qusker  33318  bnj554  34854  erdszelem9  35145  sategoelfvb  35365  mrsubff1  35460  msubff1  35502  mvhf1  35505  fneval  36294  topfneec2  36298  bj-imdirval3  37126  f1omptsnlem  37278  f1omptsn  37279  rdgeqoa  37312  poimirlem4  37572  poimirlem26  37594  poimirlem27  37595  ismtyval  37748  extep  38225  brdmqss  38588  fimgmcyc  42489  sn-isghm  42628  wepwsolem  42999  fnwe2val  43006  aomclem8  43018  onsucf1o  43230  relexp0eq  43659  sprsymrelf1  47429  fmtnof1  47468  fmtnofac1  47503  prmdvdsfmtnof1  47520  sfprmdvdsmersenne  47536  gpgedgvtx0  47965  isupwlk  47998  uspgrsprf1  48009  2zlidl  48102  rrx2xpref1o  48585  rrx2plord  48587  rrx2plordisom  48590  sphere  48614  line2ylem  48618