Theorem eqeqan12d 2745

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723

This theorem is referenced by:  eqeqan12rd  2746  eqeq12d  2747  eqeq12  2748  eqfnfv2  6965  f1mpt  7195  soisores  7261  xpopth  7962  f1o2ndf1  8052  fnwelem  8061  fnse  8063  tz7.48lem  8360  ecopoveq  8742  xpdom2  8985  unfilem2  9190  wemaplem1  9432  suc11reg  9509  oemapval  9573  cantnf  9583  wemapwe  9587  r0weon  9903  infxpen  9905  fodomacn  9947  sornom  10168  fin1a2lem2  10292  fin1a2lem4  10294  neg11  11412  subeqrev  11539  rpnnen1lem6  12880  cnref1o  12883  xneg11  13114  injresinj  13691  modadd1  13812  modaddid  13814  modmul1  13831  modlteq  13852  sq11  14038  hashen  14254  fz1eqb  14261  eqwrd  14464  s111  14523  ccatopth  14623  wrd2ind  14630  wwlktovf1  14864  cj11  15069  sqrt11  15169  sqabs  15214  recan  15244  reeff1  16029  efieq  16072  eulerthlem2  16693  vdwlem12  16904  xpsff1o  17471  ismgmhm  18604  ismhm  18693  isghm  19128  gsmsymgreq  19345  symgfixf1  19350  odf1  19475  sylow1  19516  frgpuplem  19685  isdomn  20621  rngqiprngimfo  21239  pzriprnglem11  21429  cygznlem3  21507  psgnghm  21518  tgtop11  22898  fclsval  23924  vitali  25542  recosf1o  26472  mpodvdsmulf1o  27132  dvdsmulf1o  27134  fsumvma  27152  negs11  27992  onsiso  28206  bdayn0sf1o  28296  brcgr  28879  axlowdimlem15  28935  axcontlem1  28943  axcontlem4  28946  axcontlem7  28949  axcontlem8  28950  iswlk  29590  wlkswwlksf1o  29858  wwlksnextinj  29878  clwlkclwwlkf1  29988  clwwlkf1  30027  numclwwlkqhash  30353  grpoinvf  30510  hial2eq2  31085  qusker  33312  bnj554  34909  erdszelem9  35241  sategoelfvb  35461  mrsubff1  35556  msubff1  35598  mvhf1  35601  fneval  36392  topfneec2  36396  bj-imdirval3  37224  f1omptsnlem  37376  f1omptsn  37377  rdgeqoa  37410  poimirlem4  37670  poimirlem26  37692  poimirlem27  37693  ismtyval  37846  extep  38323  brdmqss  38689  fimgmcyc  42573  sn-isghm  42712  wepwsolem  43081  fnwe2val  43088  aomclem8  43100  onsucf1o  43311  relexp0eq  43740  sprsymrelf1  47533  fmtnof1  47572  fmtnofac1  47607  prmdvdsfmtnof1  47624  sfprmdvdsmersenne  47640  gpgedgvtx0  48098  isupwlk  48173  uspgrsprf1  48184  2zlidl  48277  rrx2xpref1o  48756  rrx2plord  48758  rrx2plordisom  48761  sphere  48785  line2ylem  48789