Theorem eqeqan12d 2751

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729

This theorem is referenced by:  eqeqan12rd  2752  eqeq12d  2753  eqeq12  2754  eqfnfv2  6986  f1mpt  7217  soisores  7283  xpopth  7984  f1o2ndf1  8074  fnwelem  8083  fnse  8085  tz7.48lem  8382  ecopoveq  8767  xpdom2  9012  unfilem2  9218  wemaplem1  9463  suc11reg  9540  oemapval  9604  cantnf  9614  wemapwe  9618  r0weon  9934  infxpen  9936  fodomacn  9978  sornom  10199  fin1a2lem2  10323  fin1a2lem4  10325  neg11  11444  subeqrev  11571  rpnnen1lem6  12907  cnref1o  12910  xneg11  13142  injresinj  13719  modadd1  13840  modaddid  13842  modmul1  13859  modlteq  13880  sq11  14066  hashen  14282  fz1eqb  14289  eqwrd  14492  s111  14551  ccatopth  14651  wrd2ind  14658  wwlktovf1  14892  cj11  15097  sqrt11  15197  sqabs  15242  recan  15272  reeff1  16057  efieq  16100  eulerthlem2  16721  vdwlem12  16932  xpsff1o  17500  ismgmhm  18633  ismhm  18722  isghm  19156  gsmsymgreq  19373  symgfixf1  19378  odf1  19503  sylow1  19544  frgpuplem  19713  isdomn  20650  rngqiprngimfo  21268  pzriprnglem11  21458  cygznlem3  21536  psgnghm  21547  tgtop11  22938  fclsval  23964  vitali  25582  recosf1o  26512  mpodvdsmulf1o  27172  dvdsmulf1o  27174  fsumvma  27192  negs11  28057  oniso  28279  bdayn0sf1o  28378  brcgr  28985  axlowdimlem15  29041  axcontlem1  29049  axcontlem4  29052  axcontlem7  29055  axcontlem8  29056  iswlk  29696  wlkswwlksf1o  29964  wwlksnextinj  29984  clwlkclwwlkf1  30097  clwwlkf1  30136  numclwwlkqhash  30462  grpoinvf  30619  hial2eq2  31194  qusker  33441  bnj554  35074  erdszelem9  35412  sategoelfvb  35632  mrsubff1  35727  msubff1  35769  mvhf1  35772  fneval  36565  topfneec2  36569  bj-imdirval3  37436  f1omptsnlem  37588  f1omptsn  37589  rdgeqoa  37622  poimirlem4  37872  poimirlem26  37894  poimirlem27  37895  ismtyval  38048  extep  38537  brsucmap  38714  brdmqss  38978  disjimeceqim2  39053  qmapeldisjsim  39108  fimgmcyc  42901  sn-isghm  43028  wepwsolem  43396  fnwe2val  43403  aomclem8  43415  onsucf1o  43626  relexp0eq  44054  sprsymrelf1  47853  fmtnof1  47892  fmtnofac1  47927  prmdvdsfmtnof1  47944  sfprmdvdsmersenne  47960  gpgedgvtx0  48418  isupwlk  48493  uspgrsprf1  48504  2zlidl  48597  rrx2xpref1o  49075  rrx2plord  49077  rrx2plordisom  49080  sphere  49104  line2ylem  49108