Theorem eqeqan12d 2752

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730

This theorem is referenced by:  eqeqan12rd  2753  eqeq12d  2754  eqeq12  2755  eqfnfv2  6892  f1mpt  7115  soisores  7178  xpopth  7845  f1o2ndf1  7934  fnwelem  7943  fnse  7945  tz7.48lem  8242  ecopoveq  8565  xpdom2  8807  unfilem2  9009  wemaplem1  9235  suc11reg  9307  oemapval  9371  cantnf  9381  wemapwe  9385  r0weon  9699  infxpen  9701  fodomacn  9743  sornom  9964  fin1a2lem2  10088  fin1a2lem4  10090  neg11  11202  subeqrev  11327  rpnnen1lem6  12651  cnref1o  12654  xneg11  12878  injresinj  13436  modadd1  13556  modmul1  13572  modlteq  13593  sq11  13778  hashen  13989  fz1eqb  13997  eqwrd  14188  s111  14248  ccatopth  14357  wrd2ind  14364  wwlktovf1  14600  cj11  14801  sqrt11  14902  sqabs  14947  recan  14976  reeff1  15757  efieq  15800  eulerthlem2  16411  vdwlem12  16621  xpsff1o  17195  ismhm  18347  gsmsymgreq  18955  symgfixf1  18960  odf1  19084  sylow1  19123  frgpuplem  19293  isdomn  20478  cygznlem3  20689  psgnghm  20697  tgtop11  22040  fclsval  23067  vitali  24682  recosf1o  25596  dvdsmulf1o  26248  fsumvma  26266  brcgr  27171  axlowdimlem15  27227  axcontlem1  27235  axcontlem4  27238  axcontlem7  27241  axcontlem8  27242  iswlk  27880  wlkswwlksf1o  28145  wwlksnextinj  28165  clwlkclwwlkf1  28275  clwwlkf1  28314  numclwwlkqhash  28640  grpoinvf  28795  hial2eq2  29370  qusker  31451  bnj554  32779  erdszelem9  33061  sategoelfvb  33281  mrsubff1  33376  msubff1  33418  mvhf1  33421  fneval  34468  topfneec2  34472  bj-imdirval3  35282  f1omptsnlem  35434  f1omptsn  35435  rdgeqoa  35468  poimirlem4  35708  poimirlem26  35730  poimirlem27  35731  ismtyval  35885  extep  36345  brdmqss  36686  wepwsolem  40783  fnwe2val  40790  aomclem8  40802  relexp0eq  41198  sprsymrelf1  44836  fmtnof1  44875  fmtnofac1  44910  prmdvdsfmtnof1  44927  sfprmdvdsmersenne  44943  isupwlk  45186  uspgrsprf1  45197  ismgmhm  45225  2zlidl  45380  rrx2xpref1o  45952  rrx2plord  45954  rrx2plordisom  45957  sphere  45981  line2ylem  45985