Theorem eqeqan12d 2755

Description: A useful inference for substituting definitions into an equality. See also eqeqan12dALT 2756. (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 2754	1 ⊢ ((𝜑 ∧ 𝜓) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-9 2124  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1787  df-cleq 2730

This theorem is referenced by:  eqeqan12rd  2757  eqfnfv2  6810  f1mpt  7030  soisores  7093  xpopth  7755  f1o2ndf1  7844  fnwelem  7851  fnse  7853  tz7.48lem  8106  ecopoveq  8429  xpdom2  8661  unfilem2  8857  wemaplem1  9083  suc11reg  9155  oemapval  9219  cantnf  9229  wemapwe  9233  r0weon  9512  infxpen  9514  fodomacn  9556  sornom  9777  fin1a2lem2  9901  fin1a2lem4  9903  neg11  11015  subeqrev  11140  rpnnen1lem6  12464  cnref1o  12467  xneg11  12691  injresinj  13249  modadd1  13367  modmul1  13383  modlteq  13404  sq11  13588  hashen  13799  fz1eqb  13807  eqwrd  13998  s111  14058  ccatopth  14167  wrd2ind  14174  wwlktovf1  14410  cj11  14611  sqrt11  14712  sqabs  14757  recan  14786  reeff1  15565  efieq  15608  eulerthlem2  16219  vdwlem12  16428  xpsff1o  16943  ismhm  18074  gsmsymgreq  18678  symgfixf1  18683  odf1  18807  sylow1  18846  frgpuplem  19016  isdomn  20186  cygznlem3  20388  psgnghm  20396  tgtop11  21733  fclsval  22759  vitali  24365  recosf1o  25279  dvdsmulf1o  25931  fsumvma  25949  brcgr  26846  axlowdimlem15  26902  axcontlem1  26910  axcontlem4  26913  axcontlem7  26916  axcontlem8  26917  iswlk  27552  wlkswwlksf1o  27817  wwlksnextinj  27837  clwlkclwwlkf1  27947  clwwlkf1  27986  numclwwlkqhash  28312  grpoinvf  28467  hial2eq2  29042  qusker  31121  bnj554  32450  erdszelem9  32732  sategoelfvb  32952  mrsubff1  33047  msubff1  33089  mvhf1  33092  fneval  34179  topfneec2  34183  bj-imdirval3  34976  f1omptsnlem  35130  f1omptsn  35131  rdgeqoa  35164  poimirlem4  35404  poimirlem26  35426  poimirlem27  35427  ismtyval  35581  extep  36041  brdmqss  36382  wepwsolem  40439  fnwe2val  40446  aomclem8  40458  relexp0eq  40855  sprsymrelf1  44482  fmtnof1  44521  fmtnofac1  44556  prmdvdsfmtnof1  44573  sfprmdvdsmersenne  44589  isupwlk  44832  uspgrsprf1  44843  ismgmhm  44871  2zlidl  45026  rrx2xpref1o  45598  rrx2plord  45600  rrx2plordisom  45603  sphere  45627  line2ylem  45631