Theorem eqeqan12d 2625

Description: A useful inference for substituting definitions into an equality. See also eqeqan12dALT 2626. (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 479	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐵)
3		eqeqan12d.2	. . 3 ⊢ (𝜓 → 𝐶 = 𝐷)
4	3	adantl 480	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝐶 = 𝐷)
5	2, 4	eqeq12d 2624	1 ⊢ ((𝜑 ∧ 𝜓) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))

Syntax hints:   → wi 4   ↔ wb 194   ∧ wa 382   = wceq 1474

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-ext 2589

This theorem depends on definitions:  df-bi 195  df-an 384  df-cleq 2602

This theorem is referenced by:  eqeqan12rd  2627  eqfnfv2  6205  f1mpt  6397  soisores  6455  xpopth  7075  f1o2ndf1  7149  fnwelem  7156  fnse  7158  tz7.48lem  7400  ecopoveq  7712  xpdom2  7917  unfilem2  8087  wemaplem1  8311  suc11reg  8376  oemapval  8440  cantnf  8450  wemapwe  8454  r0weon  8695  infxpen  8697  fodomacn  8739  sornom  8959  fin1a2lem2  9083  fin1a2lem4  9085  neg11  10183  subeqrev  10304  rpnnen1lem6  11651  rpnnen1OLD  11657  cnref1o  11659  xneg11  11879  injresinj  12406  modadd1  12524  modmul1  12540  modlteq  12561  sq11  12753  hashen  12949  fz1eqb  12959  eqwrd  13147  s111  13194  wrd2ind  13275  wwlktovf1  13494  cj11  13696  sqrt11  13797  sqabs  13841  recan  13870  reeff1  14635  efieq  14678  eulerthlem2  15271  vdwlem12  15480  xpsff1o  15997  ismhm  17106  gsmsymgreq  17621  symgfixf1  17626  odf1  17748  sylow1  17787  frgpuplem  17954  isdomn  19061  cygznlem3  19682  psgnghm  19690  tgtop11  20539  fclsval  21564  vitali  23105  recosf1o  24002  dvdsmulf1o  24637  fsumvma  24655  brcgr  25498  axlowdimlem15  25554  axcontlem1  25562  axcontlem4  25565  axcontlem7  25568  axcontlem8  25569  iswlk  25814  istrl  25833  wlknwwlkninj  26005  wlkiswwlkinj  26012  wwlkextinj  26024  clwwlkf1  26090  numclwlk1lem2f1  26387  grpoinvf  26536  hial2eq2  27154  bnj554  30029  erdszelem9  30241  mrsubff1  30471  msubff1  30513  mvhf1  30516  nodenselem5  30890  fneval  31323  topfneec2  31327  f1omptsnlem  32162  f1omptsn  32163  rdgeqoa  32197  poimirlem4  32386  poimirlem26  32408  poimirlem27  32409  ismtyval  32572  wepwsolem  36433  fnwe2val  36440  aomclem8  36452  relexp0eq  36815  fmtnof1  39790  fmtnofac1  39825  prmdvdsfmtnof1  39842  sfprmdvdsmersenne  39863  is1wlk  40815  isWlk  40816  1wlkpwwlkf1ouspgr  41078  wlknwwlksninj  41088  wlkwwlkinj  41095  wwlksnextinj  41107  clwwlksf1  41226  av-numclwlk1lem2f1  41526  ismgmhm  41575  2zlidl  41726