Theorem eqeqan12d 2837

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-9 2123  ax-ext 2792

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1780  df-cleq 2813

This theorem is referenced by:  eqeqan12rd  2839  eqfnfv2  6796  f1mpt  7012  soisores  7073  xpopth  7723  f1o2ndf1  7811  fnwelem  7818  fnse  7820  tz7.48lem  8070  ecopoveq  8391  xpdom2  8605  unfilem2  8776  wemaplem1  9003  suc11reg  9075  oemapval  9139  cantnf  9149  wemapwe  9153  r0weon  9431  infxpen  9433  fodomacn  9475  sornom  9692  fin1a2lem2  9816  fin1a2lem4  9818  neg11  10930  subeqrev  11055  rpnnen1lem6  12375  cnref1o  12378  xneg11  12602  injresinj  13155  modadd1  13273  modmul1  13289  modlteq  13310  sq11  13493  hashen  13704  fz1eqb  13712  eqwrd  13904  s111  13964  ccatopth  14073  wrd2ind  14080  wwlktovf1  14316  cj11  14516  sqrt11  14617  sqabs  14662  recan  14691  reeff1  15468  efieq  15511  eulerthlem2  16114  vdwlem12  16323  xpsff1o  16835  ismhm  17953  gsmsymgreq  18555  symgfixf1  18560  odf1  18684  sylow1  18723  frgpuplem  18893  isdomn  20062  cygznlem3  20711  psgnghm  20719  tgtop11  21585  fclsval  22611  vitali  24209  recosf1o  25117  dvdsmulf1o  25769  fsumvma  25787  brcgr  26684  axlowdimlem15  26740  axcontlem1  26748  axcontlem4  26751  axcontlem7  26754  axcontlem8  26755  iswlk  27390  wlkswwlksf1o  27655  wwlksnextinj  27675  clwlkclwwlkf1  27786  clwwlkf1  27826  numclwwlkqhash  28152  grpoinvf  28307  hial2eq2  28882  qusker  30939  bnj554  32192  erdszelem9  32467  sategoelfvb  32687  mrsubff1  32782  msubff1  32824  mvhf1  32827  fneval  33721  topfneec2  33725  bj-imdirval3  34498  f1omptsnlem  34641  f1omptsn  34642  rdgeqoa  34675  poimirlem4  34931  poimirlem26  34953  poimirlem27  34954  ismtyval  35111  extep  35573  brdmqss  35914  wepwsolem  39718  fnwe2val  39725  aomclem8  39737  relexp0eq  40120  sprsymrelf1  43732  fmtnof1  43771  fmtnofac1  43806  prmdvdsfmtnof1  43823  sfprmdvdsmersenne  43842  isupwlk  44085  uspgrsprf1  44096  ismgmhm  44124  2zlidl  44279  rrx2xpref1o  44779  rrx2plord  44781  rrx2plordisom  44784  sphere  44808  line2ylem  44812