Theorem eqeqan12d 2776

Description: A useful inference for substituting definitions into an equality. See also eqeqan12dALT 2777. (Contributed by NM, 9-Aug-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 20-Nov-2019.)

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	adantr 472	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐵)
3		eqeqan12d.2	. . 3 ⊢ (𝜓 → 𝐶 = 𝐷)
4	3	adantl 473	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝐶 = 𝐷)
5	2, 4	eqeq12d 2775	1 ⊢ ((𝜑 ∧ 𝜓) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1632

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1854  df-cleq 2753

This theorem is referenced by:  eqeqan12rd  2778  eqfnfv2  6475  f1mpt  6681  soisores  6740  xpopth  7374  f1o2ndf1  7453  fnwelem  7460  fnse  7462  tz7.48lem  7705  ecopoveq  8015  xpdom2  8220  unfilem2  8390  wemaplem1  8616  suc11reg  8689  oemapval  8753  cantnf  8763  wemapwe  8767  r0weon  9025  infxpen  9027  fodomacn  9069  sornom  9291  fin1a2lem2  9415  fin1a2lem4  9417  neg11  10524  subeqrev  10645  rpnnen1lem6  12012  rpnnen1OLD  12018  cnref1o  12020  xneg11  12239  injresinj  12783  modadd1  12901  modmul1  12917  modlteq  12938  sq11  13130  hashen  13329  fz1eqb  13337  eqwrd  13533  s111  13586  wrd2ind  13677  wwlktovf1  13901  cj11  14101  sqrt11  14202  sqabs  14246  recan  14275  reeff1  15049  efieq  15092  eulerthlem2  15689  vdwlem12  15898  xpsff1o  16430  ismhm  17538  gsmsymgreq  18052  symgfixf1  18057  odf1  18179  sylow1  18218  frgpuplem  18385  isdomn  19496  cygznlem3  20120  psgnghm  20128  tgtop11  20988  fclsval  22013  vitali  23581  recosf1o  24480  dvdsmulf1o  25119  fsumvma  25137  brcgr  25979  axlowdimlem15  26035  axcontlem1  26043  axcontlem4  26046  axcontlem7  26049  axcontlem8  26050  iswlk  26716  wlkpwwlkf1ouspgr  26988  wlknwwlksninj  26998  wlkwwlkinj  27005  wwlksnextinj  27017  clwlkclwwlkf1  27133  clwwlkf1  27178  numclwwlkqhash  27536  grpoinvf  27695  hial2eq2  28273  bnj554  31276  erdszelem9  31488  mrsubff1  31718  msubff1  31760  mvhf1  31763  fneval  32653  topfneec2  32657  f1omptsnlem  33494  f1omptsn  33495  rdgeqoa  33529  poimirlem4  33726  poimirlem26  33748  poimirlem27  33749  ismtyval  33912  extep  34372  wepwsolem  38114  fnwe2val  38121  aomclem8  38133  relexp0eq  38495  fmtnof1  41957  fmtnofac1  41992  prmdvdsfmtnof1  42009  sfprmdvdsmersenne  42030  isupwlk  42227  sprsymrelf1  42256  uspgrsprf1  42265  ismgmhm  42293  2zlidl  42444