Theorem eqeq12i 2781

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 2768	. 2 ⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐶)
3		eqeq12i.2	. . 3 ⊢ 𝐶 = 𝐷
4	3	eqeq2i 2776	. 2 ⊢ (𝐵 = 𝐶 ↔ 𝐵 = 𝐷)
5	2, 4	bitri 278	1 ⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐷)

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755

This theorem is used by:  neeq12i  3025  rabbi  3445  unineq  4236  vn0  4294  vn0OLD  4295  sbceqg  4373  sbceqi  4374  preq2b  4805  preqr2  4807  otth  5457  otthg  5458  rncoeq  5972  fresaunres1  6777  eqfnov  7572  mpo2eqb  7575  f1o2ndf1  8160  fprlem1  8346  ecopovsym  8868  frrlem15  9788  kardenOLD  9987  adderpqlem  11066  mulerpqlem  11067  addcmpblnr  11181  ax1ne0  11272  addrid  11517  sq11i  14361  nn0opth2i  14442  degenmgmnfn  19165  oppgcntz  19608  opprdomnb  20998  isdomn4r  21000  islpir  21682  evlsval  22425  volfiniun  25898  dvmptfsum  26325  ltsval2  28043  ltssolem1  28062  nosepnelem  28066  nolt02o  28082  axlowdimlem13  29562  usgredg2v  29838  issubgr  29882  clwlkcompbp  30399  pjneli  32355  indifbi  33188  madjusmdetlem1  34529  breprexp  35332  bnj553  35598  bnj1253  35717  gonanegoal  36284  goalrlem  36328  goalr  36329  fmlasucdisj  36331  satffunlem  36333  satffunlem1lem1  36334  satffunlem2lem1  36336  altopthsn  36904  bj-2upleq  38103  bj-vn0ALT  38178  relowlpssretop  38479  iscrngo2  39123  extid  39440  cdleme18d  41544  fphpd  44016  oenassex  44512  rp-fakeuninass  44709  relexp0eq  44893  comptiunov2i  44898  clsk1indlem1  45237  ntrclskb  45261  onfrALTlem5  45716  onfrALTlem4  45717  onfrALTlem5VD  46058  onfrALTlem4VD  46059  dvnprodlem3  47163  sge0xadd  47650  reuabaiotaiota  48362  rrx2linest  50059  fucofvalne  50652