Theorem eqeqan12d 2840

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2816

This theorem is referenced by:  eqeqan12rd  2842  eqfnfv2  6805  f1mpt  7021  soisores  7082  xpopth  7732  f1o2ndf1  7820  fnwelem  7827  fnse  7829  tz7.48lem  8079  ecopoveq  8400  xpdom2  8614  unfilem2  8785  wemaplem1  9012  suc11reg  9084  oemapval  9148  cantnf  9158  wemapwe  9162  r0weon  9440  infxpen  9442  fodomacn  9484  sornom  9701  fin1a2lem2  9825  fin1a2lem4  9827  neg11  10939  subeqrev  11064  rpnnen1lem6  12384  cnref1o  12387  xneg11  12611  injresinj  13161  modadd1  13279  modmul1  13295  modlteq  13316  sq11  13499  hashen  13710  fz1eqb  13718  eqwrd  13911  s111  13971  ccatopth  14080  wrd2ind  14087  wwlktovf1  14323  cj11  14523  sqrt11  14624  sqabs  14669  recan  14698  reeff1  15475  efieq  15518  eulerthlem2  16121  vdwlem12  16330  xpsff1o  16842  ismhm  17960  gsmsymgreq  18562  symgfixf1  18567  odf1  18691  sylow1  18730  frgpuplem  18900  isdomn  20069  cygznlem3  20718  psgnghm  20726  tgtop11  21592  fclsval  22618  vitali  24216  recosf1o  25121  dvdsmulf1o  25773  fsumvma  25791  brcgr  26688  axlowdimlem15  26744  axcontlem1  26752  axcontlem4  26755  axcontlem7  26758  axcontlem8  26759  iswlk  27394  wlkswwlksf1o  27659  wwlksnextinj  27679  clwlkclwwlkf1  27790  clwwlkf1  27830  numclwwlkqhash  28156  grpoinvf  28311  hial2eq2  28886  qusker  30920  bnj554  32173  erdszelem9  32448  sategoelfvb  32668  mrsubff1  32763  msubff1  32805  mvhf1  32808  fneval  33702  topfneec2  33706  bj-imdirval3  34476  f1omptsnlem  34619  f1omptsn  34620  rdgeqoa  34653  poimirlem4  34898  poimirlem26  34920  poimirlem27  34921  ismtyval  35080  extep  35542  brdmqss  35883  wepwsolem  39649  fnwe2val  39656  aomclem8  39668  relexp0eq  40053  sprsymrelf1  43665  fmtnof1  43704  fmtnofac1  43739  prmdvdsfmtnof1  43756  sfprmdvdsmersenne  43775  isupwlk  44018  uspgrsprf1  44029  ismgmhm  44057  2zlidl  44212  rrx2xpref1o  44712  rrx2plord  44714  rrx2plordisom  44717  sphere  44741  line2ylem  44745