Theorem eqeqan12d 2626

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

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-an 385  df-cleq 2603

This theorem is referenced by:  eqeqan12rd  2628  eqfnfv2  6220  f1mpt  6419  soisores  6477  xpopth  7098  f1o2ndf1  7172  fnwelem  7179  fnse  7181  tz7.48lem  7423  ecopoveq  7735  xpdom2  7940  unfilem2  8110  wemaplem1  8334  suc11reg  8399  oemapval  8463  cantnf  8473  wemapwe  8477  r0weon  8718  infxpen  8720  fodomacn  8762  sornom  8982  fin1a2lem2  9106  fin1a2lem4  9108  neg11  10211  subeqrev  10332  rpnnen1lem6  11695  rpnnen1OLD  11701  cnref1o  11703  xneg11  11920  injresinj  12451  modadd1  12569  modmul1  12585  modlteq  12606  sq11  12798  hashen  12997  fz1eqb  13007  eqwrd  13201  s111  13248  wrd2ind  13329  wwlktovf1  13548  cj11  13750  sqrt11  13851  sqabs  13895  recan  13924  reeff1  14689  efieq  14732  eulerthlem2  15325  vdwlem12  15534  xpsff1o  16051  ismhm  17160  gsmsymgreq  17675  symgfixf1  17680  odf1  17802  sylow1  17841  frgpuplem  18008  isdomn  19115  cygznlem3  19737  psgnghm  19745  tgtop11  20597  fclsval  21622  vitali  23188  recosf1o  24085  dvdsmulf1o  24720  fsumvma  24738  brcgr  25580  axlowdimlem15  25636  axcontlem1  25644  axcontlem4  25647  axcontlem7  25650  axcontlem8  25651  iswlk  26048  istrl  26067  wlknwwlkninj  26239  wlkiswwlkinj  26246  wwlkextinj  26258  clwwlkf1  26324  numclwlk1lem2f1  26621  grpoinvf  26770  hial2eq2  27348  bnj554  30223  erdszelem9  30435  mrsubff1  30665  msubff1  30707  mvhf1  30710  nodenselem5  31084  fneval  31517  topfneec2  31521  f1omptsnlem  32359  f1omptsn  32360  rdgeqoa  32394  poimirlem4  32583  poimirlem26  32605  poimirlem27  32606  ismtyval  32769  wepwsolem  36630  fnwe2val  36637  aomclem8  36649  relexp0eq  37012  fmtnof1  39985  fmtnofac1  40020  prmdvdsfmtnof1  40037  sfprmdvdsmersenne  40058  is1wlk  40813  isWlk  40814  1wlkpwwlkf1ouspgr  41076  wlknwwlksninj  41086  wlkwwlkinj  41093  wwlksnextinj  41105  clwwlksf1  41224  av-numclwlk1lem2f1  41524  ismgmhm  41573  2zlidl  41724