Theorem eqeq12i 2780

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 2767	. 2 ⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐶)
3		eqeq12i.2	. . 3 ⊢ 𝐶 = 𝐷
4	3	eqeq2i 2775	. 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 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2734

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

This theorem is used by:  neeq12i  3023  rabbi  3444  unineq  4237  vn0  4294  vn0OLD  4295  sbceqg  4373  sbceqi  4374  preq2b  4810  preqr2  4812  otth  5464  otthg  5465  rncoeq  5969  fresaunres1  6752  eqfnov  7545  mpo2eqb  7548  f1o2ndf1  8122  fprlem1  8302  ecopovsym  8822  frrlem15  9742  kardenOLD  9902  adderpqlem  10966  mulerpqlem  10967  addcmpblnr  11081  ax1ne0  11172  addrid  11417  sq11i  14257  nn0opth2i  14337  degenmgmnfn  19050  oppgcntz  19492  opprdomnb  20879  isdomn4r  20881  islpir  21560  evlsval  22303  volfiniun  25776  dvmptfsum  26204  ltsval2  27890  ltssolem1  27909  nosepnelem  27913  nolt02o  27929  axlowdimlem13  29397  usgredg2v  29673  issubgr  29717  clwlkcompbp  30234  pjneli  32190  indifbi  32981  madjusmdetlem1  34324  breprexp  35128  bnj553  35394  bnj1253  35513  gonanegoal  35918  goalrlem  35962  goalr  35963  fmlasucdisj  35965  satffunlem  35967  satffunlem1lem1  35968  satffunlem2lem1  35970  altopthsn  36528  bj-2upleq  37743  bj-vn0ALT  37803  relowlpssretop  38105  iscrngo2  38734  extid  39051  cdleme18d  41155  fphpd  43644  oenassex  44146  rp-fakeuninass  44343  relexp0eq  44528  comptiunov2i  44533  clsk1indlem1  44872  ntrclskb  44896  onfrALTlem5  45352  onfrALTlem4  45353  onfrALTlem5VD  45694  onfrALTlem4VD  45695  dvnprodlem3  46763  sge0xadd  47250  reuabaiotaiota  47962  rrx2linest  49659  fucofvalne  50238