Theorem eqeqan12d 2777

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755

This theorem is used by:  eqeqan12rd  2778  eqeq12d  2779  eqeq12  2780  eqfnfv2  7056  f1mpt  7291  soisores  7361  xpopth  8069  f1o2ndf1  8163  fnwelem  8173  fnwe2lem1  8175  fnse  8180  onelfvnef1  8480  tz7.48lem  8481  tz7.48lemOLD  8482  ecopoveq  8870  xpdom2  9122  unfilem2  9329  wemaplem1  9570  suc11reg  9650  oemapval  9714  cantnf  9724  wemapwe  9728  r0weon  10121  infxpen  10123  fodomacn  10165  sornom  10385  fin1a2lem2  10509  fin1a2lem4  10511  neg11  11639  subeqrev  11768  rpnnen1lem6  13140  cnref1o  13143  xneg11  13375  injresinj  13956  modadd1  14078  modaddid  14080  modmul1  14097  modlteq  14118  sq11  14304  hashen  14521  fz1eqb  14528  eqwrd  14732  s111  14794  ccatopth  14896  wrd2ind  14903  wwlktovf1  15142  cj11  15361  sqrt11  15461  sqabs  15506  recan  15536  reeff1  16320  efieq  16363  eulerthlem2  16991  vdwlem12  17202  xpsff1o  17771  ismgmhm  18917  ismhm  19012  isghm  19462  gsmsymgreq  19679  symgfixf1  19684  odf1  19809  sylow1  19850  frgpuplem  20019  rhmval0  20738  isdomn  20990  rngqiprngimfo  21630  pzriprnglem11  21830  cygznlem3  21908  psgnghm  21919  tgtop11  23333  fclsval  24360  vitali  25967  recosf1o  26896  mpodvdsmulf1o  27554  dvdsmulf1o  27556  fsumvma  27573  negs11  28468  oniso  28690  bdayn0sf1o  28789  brcgr  29511  axlowdimlem15  29567  axcontlem1  29575  axcontlem4  29578  axcontlem7  29581  axcontlem8  29582  iswlk  30224  wlkswwlksf1o  30501  wwlksnextinj  30521  clwlkclwwlkf1  30634  clwwlkf1  30673  numclwwlkqhash  31009  grpoinvf  31167  hial2eq2  31742  qusker  33994  bnj554  35612  jaeqifi  35795  erdszelem9  36144  sategoelfvb  36364  mrsubff1  36459  msubff1  36501  mvhf1  36504  fneval  37331  topfneec2  37335  bj-imdirval3  38310  f1omptsnlem  38464  f1omptsn  38465  rdgeqoa  38498  poimirlem4  38747  poimirlem26  38769  poimirlem27  38770  ismtyval  38937  extep  39424  brsucmap  39601  brdmqss  39865  disjimeceqim2  39940  qmapeldisjsim  39995  fimgmcyc  43802  sn-isghm  43888  wepwsolem  44253  aomclem8  44267  onsucf1o  44477  relexp0eq  44904  sprsymrelf1  48793  fmtnof1  48835  fmtnofac1  48870  prmdvdsfmtnof1  48887  sfprmdvdsmersenne  48903  gpgedgvtx0  49374  isupwlk  49449  uspgrsprf1  49460  2zlidl  49552  rrx2plord  50048  rrx2plordisom  50051  sphere  50074  line2ylem  50078