Theorem eqeq12i 2754

Description: A useful inference for substituting definitions into an equality. (Contributed by NM, 15-Jul-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 20-Nov-2019.)

Hypotheses

Ref	Expression
eqeq12i.1	⊢ 𝐴 = 𝐵
eqeq12i.2	⊢ 𝐶 = 𝐷

Assertion

Ref	Expression
eqeq12i	⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐷)

Proof of Theorem eqeq12i

Step	Hyp	Ref	Expression
1		eqeq12i.1	. . 3 ⊢ 𝐴 = 𝐵
2	1	eqeq1i 2741	. 2 ⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐶)
3		eqeq12i.2	. . 3 ⊢ 𝐶 = 𝐷
4	3	eqeq2i 2749	. 2 ⊢ (𝐵 = 𝐶 ↔ 𝐵 = 𝐷)
5	2, 4	bitri 275	1 ⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐷)

Syntax hints:   ↔ wb 206   = wceq 1541

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 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728

This theorem is referenced by:  neeq12i  2998  rabbi  3429  unineq  4240  vn0  4297  sbceqg  4364  sbceqi  4365  preq2b  4803  preqr2  4805  otth  5432  otthg  5433  rncoeq  5931  fresaunres1  6707  eqfnov  7487  mpo2eqb  7490  f1o2ndf1  8064  fprlem1  8242  ecopovsym  8756  frrlem15  9669  karden  9807  adderpqlem  10865  mulerpqlem  10866  addcmpblnr  10980  ax1ne0  11071  addrid  11313  sq11i  14114  nn0opth2i  14194  oppgcntz  19293  opprdomnb  20650  isdomn4r  20652  islpir  21283  evlsval  22041  volfiniun  25504  dvmptfsum  25935  ltsval2  27624  ltssolem1  27643  nosepnelem  27647  nolt02o  27663  axlowdimlem13  29027  usgredg2v  29300  issubgr  29344  clwlkcompbp  29855  pjneli  31798  indifbi  32595  madjusmdetlem1  33984  breprexp  34790  bnj553  35054  bnj1253  35173  gonanegoal  35546  goalrlem  35590  goalr  35591  fmlasucdisj  35593  satffunlem  35595  satffunlem1lem1  35596  satffunlem2lem1  35598  altopthsn  36155  bj-2upleq  37213  relowlpssretop  37569  iscrngo2  38198  extid  38509  cdleme18d  40555  fphpd  43058  oenassex  43560  rp-fakeuninass  43757  relexp0eq  43942  comptiunov2i  43947  clsk1indlem1  44286  ntrclskb  44310  onfrALTlem5  44783  onfrALTlem4  44784  onfrALTlem5VD  45125  onfrALTlem4VD  45126  dvnprodlem3  46192  sge0xadd  46679  reuabaiotaiota  47333  rrx2linest  48988  fucofvalne  49570