Theorem eqeqan12d 2815

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791

This theorem is referenced by:  eqeqan12rd  2817  eqfnfv2  6780  f1mpt  6997  soisores  7059  xpopth  7712  f1o2ndf1  7801  fnwelem  7808  fnse  7810  tz7.48lem  8060  ecopoveq  8381  xpdom2  8595  unfilem2  8767  wemaplem1  8994  suc11reg  9066  oemapval  9130  cantnf  9140  wemapwe  9144  r0weon  9423  infxpen  9425  fodomacn  9467  sornom  9688  fin1a2lem2  9812  fin1a2lem4  9814  neg11  10926  subeqrev  11051  rpnnen1lem6  12369  cnref1o  12372  xneg11  12596  injresinj  13153  modadd1  13271  modmul1  13287  modlteq  13308  sq11  13492  hashen  13703  fz1eqb  13711  eqwrd  13900  s111  13960  ccatopth  14069  wrd2ind  14076  wwlktovf1  14312  cj11  14513  sqrt11  14614  sqabs  14659  recan  14688  reeff1  15465  efieq  15508  eulerthlem2  16109  vdwlem12  16318  xpsff1o  16832  ismhm  17950  gsmsymgreq  18552  symgfixf1  18557  odf1  18681  sylow1  18720  frgpuplem  18890  isdomn  20060  cygznlem3  20261  psgnghm  20269  tgtop11  21587  fclsval  22613  vitali  24217  recosf1o  25127  dvdsmulf1o  25779  fsumvma  25797  brcgr  26694  axlowdimlem15  26750  axcontlem1  26758  axcontlem4  26761  axcontlem7  26764  axcontlem8  26765  iswlk  27400  wlkswwlksf1o  27665  wwlksnextinj  27685  clwlkclwwlkf1  27795  clwwlkf1  27834  numclwwlkqhash  28160  grpoinvf  28315  hial2eq2  28890  qusker  30969  bnj554  32281  erdszelem9  32559  sategoelfvb  32779  mrsubff1  32874  msubff1  32916  mvhf1  32919  fneval  33813  topfneec2  33817  bj-imdirval3  34599  f1omptsnlem  34753  f1omptsn  34754  rdgeqoa  34787  poimirlem4  35061  poimirlem26  35083  poimirlem27  35084  ismtyval  35238  extep  35700  brdmqss  36041  wepwsolem  39986  fnwe2val  39993  aomclem8  40005  relexp0eq  40402  sprsymrelf1  44013  fmtnof1  44052  fmtnofac1  44087  prmdvdsfmtnof1  44104  sfprmdvdsmersenne  44121  isupwlk  44364  uspgrsprf1  44375  ismgmhm  44403  2zlidl  44558  rrx2xpref1o  45132  rrx2plord  45134  rrx2plordisom  45137  sphere  45161  line2ylem  45165