Theorem eqeqan12d 2754

Description: A useful inference for substituting definitions into an equality. See also eqeqan12dALT 2759. (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 514	1 ⊢ ((𝜑 ∧ 𝜓) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1547

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732

This theorem is referenced by:  eqeqan12rd  2755  eqeq12d  2756  eqeq12  2757  eqfnfv2  6979  f1mpt  7212  soisores  7278  xpopth  7979  f1o2ndf1  8068  fnwelem  8078  fnse  8080  tz7.48lem  8377  ecopoveq  8762  xpdom2  9007  unfilem2  9213  wemaplem1  9458  suc11reg  9538  oemapval  9602  cantnf  9612  wemapwe  9616  r0weon  9932  infxpen  9934  fodomacn  9976  sornom  10197  fin1a2lem2  10321  fin1a2lem4  10323  neg11  11443  subeqrev  11570  rpnnen1lem6  12930  cnref1o  12933  xneg11  13165  injresinj  13744  modadd1  13865  modaddid  13867  modmul1  13884  modlteq  13905  sq11  14091  hashen  14307  fz1eqb  14314  eqwrd  14517  s111  14576  ccatopth  14676  wrd2ind  14683  wwlktovf1  14917  cj11  15122  sqrt11  15222  sqabs  15267  recan  15297  reeff1  16085  efieq  16128  eulerthlem2  16750  vdwlem12  16961  xpsff1o  17529  ismgmhm  18662  ismhm  18751  isghm  19188  gsmsymgreq  19405  symgfixf1  19410  odf1  19535  sylow1  19576  frgpuplem  19745  isdomn  20684  rngqiprngimfo  21301  pzriprnglem11  21473  cygznlem3  21551  psgnghm  21562  tgtop11  22972  fclsval  23998  vitali  25605  recosf1o  26524  mpodvdsmulf1o  27182  dvdsmulf1o  27184  fsumvma  27201  negs11  28066  oniso  28288  bdayn0sf1o  28387  brcgr  28994  axlowdimlem15  29050  axcontlem1  29058  axcontlem4  29061  axcontlem7  29064  axcontlem8  29065  iswlk  29704  wlkswwlksf1o  29972  wwlksnextinj  29992  clwlkclwwlkf1  30105  clwwlkf1  30144  numclwwlkqhash  30470  grpoinvf  30628  hial2eq2  31203  qusker  33439  bnj554  35088  erdszelem9  35434  sategoelfvb  35654  mrsubff1  35749  msubff1  35791  mvhf1  35794  fneval  36587  topfneec2  36591  bj-imdirval3  37551  f1omptsnlem  37705  f1omptsn  37706  rdgeqoa  37739  poimirlem4  37998  poimirlem26  38020  poimirlem27  38021  ismtyval  38174  extep  38663  brsucmap  38840  brdmqss  39104  disjimeceqim2  39179  qmapeldisjsim  39234  fimgmcyc  43027  sn-isghm  43130  wepwsolem  43494  fnwe2val  43501  aomclem8  43513  onsucf1o  43724  relexp0eq  44152  sprsymrelf1  47978  fmtnof1  48020  fmtnofac1  48055  prmdvdsfmtnof1  48072  sfprmdvdsmersenne  48088  gpgedgvtx0  48559  isupwlk  48634  uspgrsprf1  48645  2zlidl  48738  rrx2xpref1o  49216  rrx2plord  49218  rrx2plordisom  49221  sphere  49245  line2ylem  49249