Theorem eqeqan12d 2638

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

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   = wceq 1483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615

This theorem is referenced by:  eqeqan12rd  2640  eqfnfv2  6312  f1mpt  6518  soisores  6577  xpopth  7207  f1o2ndf1  7285  fnwelem  7292  fnse  7294  tz7.48lem  7536  ecopoveq  7848  xpdom2  8055  unfilem2  8225  wemaplem1  8451  suc11reg  8516  oemapval  8580  cantnf  8590  wemapwe  8594  r0weon  8835  infxpen  8837  fodomacn  8879  sornom  9099  fin1a2lem2  9223  fin1a2lem4  9225  neg11  10332  subeqrev  10453  rpnnen1lem6  11819  rpnnen1OLD  11825  cnref1o  11827  xneg11  12046  injresinj  12589  modadd1  12707  modmul1  12723  modlteq  12744  sq11  12936  hashen  13135  fz1eqb  13145  eqwrd  13346  s111  13395  wrd2ind  13477  wwlktovf1  13700  cj11  13902  sqrt11  14003  sqabs  14047  recan  14076  reeff1  14850  efieq  14893  eulerthlem2  15487  vdwlem12  15696  xpsff1o  16228  ismhm  17337  gsmsymgreq  17852  symgfixf1  17857  odf1  17979  sylow1  18018  frgpuplem  18185  isdomn  19294  cygznlem3  19918  psgnghm  19926  tgtop11  20786  fclsval  21812  vitali  23382  recosf1o  24281  dvdsmulf1o  24920  fsumvma  24938  brcgr  25780  axlowdimlem15  25836  axcontlem1  25844  axcontlem4  25847  axcontlem7  25850  axcontlem8  25851  iswlk  26506  wlkpwwlkf1ouspgr  26765  wlknwwlksninj  26775  wlkwwlkinj  26782  wwlksnextinj  26794  clwwlksf1  26917  numclwlk1lem2f1  27227  grpoinvf  27386  hial2eq2  27964  bnj554  30969  erdszelem9  31181  mrsubff1  31411  msubff1  31453  mvhf1  31456  fneval  32347  topfneec2  32351  f1omptsnlem  33183  f1omptsn  33184  rdgeqoa  33218  poimirlem4  33413  poimirlem26  33435  poimirlem27  33436  ismtyval  33599  extep  34048  opideq  34110  wepwsolem  37612  fnwe2val  37619  aomclem8  37631  relexp0eq  37993  fmtnof1  41447  fmtnofac1  41482  prmdvdsfmtnof1  41499  sfprmdvdsmersenne  41520  isupwlk  41717  sprsymrelf1  41746  uspgrsprf1  41755  ismgmhm  41783  2zlidl  41934