Theorem eqeqan12d 2754

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732

This theorem is referenced by:  eqeqan12rd  2755  eqeq12d  2756  eqeq12  2757  eqfnfv2  7065  f1mpt  7298  soisores  7363  xpopth  8071  f1o2ndf1  8163  fnwelem  8172  fnse  8174  tz7.48lem  8497  ecopoveq  8876  xpdom2  9133  unfilem2  9372  wemaplem1  9615  suc11reg  9688  oemapval  9752  cantnf  9762  wemapwe  9766  r0weon  10081  infxpen  10083  fodomacn  10125  sornom  10346  fin1a2lem2  10470  fin1a2lem4  10472  neg11  11587  subeqrev  11712  rpnnen1lem6  13047  cnref1o  13050  xneg11  13277  injresinj  13838  modadd1  13959  modmul1  13975  modlteq  13996  sq11  14181  hashen  14396  fz1eqb  14403  eqwrd  14605  s111  14663  ccatopth  14764  wrd2ind  14771  wwlktovf1  15006  cj11  15211  sqrt11  15311  sqabs  15356  recan  15385  reeff1  16168  efieq  16211  eulerthlem2  16829  vdwlem12  17039  xpsff1o  17627  ismgmhm  18734  ismhm  18820  isghm  19255  gsmsymgreq  19474  symgfixf1  19479  odf1  19604  sylow1  19645  frgpuplem  19814  isdomn  20727  rngqiprngimfo  21334  pzriprnglem11  21525  cygznlem3  21611  psgnghm  21621  tgtop11  23010  fclsval  24037  vitali  25667  recosf1o  26595  mpodvdsmulf1o  27255  dvdsmulf1o  27257  fsumvma  27275  negs11  28099  brcgr  28933  axlowdimlem15  28989  axcontlem1  28997  axcontlem4  29000  axcontlem7  29003  axcontlem8  29004  iswlk  29646  wlkswwlksf1o  29912  wwlksnextinj  29932  clwlkclwwlkf1  30042  clwwlkf1  30081  numclwwlkqhash  30407  grpoinvf  30564  hial2eq2  31139  qusker  33342  bnj554  34875  erdszelem9  35167  sategoelfvb  35387  mrsubff1  35482  msubff1  35524  mvhf1  35527  fneval  36318  topfneec2  36322  bj-imdirval3  37150  f1omptsnlem  37302  f1omptsn  37303  rdgeqoa  37336  poimirlem4  37584  poimirlem26  37606  poimirlem27  37607  ismtyval  37760  extep  38239  brdmqss  38602  fimgmcyc  42489  sn-isghm  42628  wepwsolem  42999  fnwe2val  43006  aomclem8  43018  onsucf1o  43234  relexp0eq  43663  sprsymrelf1  47370  fmtnof1  47409  fmtnofac1  47444  prmdvdsfmtnof1  47461  sfprmdvdsmersenne  47477  isupwlk  47859  uspgrsprf1  47870  2zlidl  47963  rrx2xpref1o  48452  rrx2plord  48454  rrx2plordisom  48457  sphere  48481  line2ylem  48485