Theorem eqeqan12d 2775

Description: A useful inference for substituting definitions into an equality. See also eqeqan12dALT 2780. (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 2763	. 2 ⊢ (𝜑 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))
3		eqeqan12d.2	. . 3 ⊢ (𝜓 → 𝐶 = 𝐷)
4	3	eqeq2d 2772	. 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 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

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

This theorem is used by:  eqeqan12rd  2776  eqeq12d  2777  eqeq12  2778  eqfnfv2  7022  f1mpt  7257  soisores  7327  xpopth  8031  f1o2ndf1  8122  fnwelem  8132  fnse  8134  onelfvnef1  8433  tz7.48lem  8434  tz7.48lemOLD  8435  ecopoveq  8823  xpdom2  9075  unfilem2  9282  wemaplem1  9524  suc11reg  9604  oemapval  9668  cantnf  9678  wemapwe  9682  r0weon  10072  infxpen  10074  fodomacn  10116  sornom  10336  fin1a2lem2  10460  fin1a2lem4  10462  neg11  11590  subeqrev  11719  rpnnen1lem6  13091  cnref1o  13094  xneg11  13326  injresinj  13906  modadd1  14028  modaddid  14030  modmul1  14047  modlteq  14068  sq11  14254  hashen  14471  fz1eqb  14478  eqwrd  14682  s111  14743  ccatopth  14845  wrd2ind  14852  wwlktovf1  15090  cj11  15309  sqrt11  15409  sqabs  15454  recan  15484  reeff1  16268  efieq  16311  eulerthlem2  16939  vdwlem12  17150  xpsff1o  17719  ismgmhm  18865  ismhm  18960  isghm  19410  gsmsymgreq  19626  symgfixf1  19631  odf1  19756  sylow1  19797  frgpuplem  19966  rhmval0  20685  isdomn  20937  rngqiprngimfo  21577  pzriprnglem11  21777  cygznlem3  21855  psgnghm  21866  tgtop11  23280  fclsval  24307  vitali  25914  recosf1o  26845  mpodvdsmulf1o  27503  dvdsmulf1o  27505  fsumvma  27522  negs11  28417  oniso  28639  bdayn0sf1o  28738  brcgr  29460  axlowdimlem15  29516  axcontlem1  29524  axcontlem4  29527  axcontlem7  29530  axcontlem8  29531  iswlk  30173  wlkswwlksf1o  30450  wwlksnextinj  30470  clwlkclwwlkf1  30583  clwwlkf1  30622  numclwwlkqhash  30958  grpoinvf  31116  hial2eq2  31691  qusker  33892  bnj554  35512  erdszelem9  35933  sategoelfvb  36153  mrsubff1  36248  msubff1  36290  mvhf1  36293  fneval  37110  topfneec2  37114  bj-imdirval3  38073  f1omptsnlem  38227  f1omptsn  38228  rdgeqoa  38261  poimirlem4  38510  poimirlem26  38532  poimirlem27  38533  ismtyval  38702  extep  39189  brsucmap  39366  brdmqss  39630  disjimeceqim2  39705  qmapeldisjsim  39760  fimgmcyc  43560  sn-isghm  43638  wepwsolem  44002  fnwe2val  44009  aomclem8  44021  onsucf1o  44232  relexp0eq  44660  sprsymrelf1  48522  fmtnof1  48564  fmtnofac1  48599  prmdvdsfmtnof1  48616  sfprmdvdsmersenne  48632  gpgedgvtx0  49103  isupwlk  49178  uspgrsprf1  49189  2zlidl  49281  rrx2xpref1o  49774  rrx2plord  49776  rrx2plordisom  49779  sphere  49803  line2ylem  49807