Theorem eqeq12i 2789

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

Syntax hints:   ↔ wb 198   = wceq 1507

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-9 2057  ax-ext 2747

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-cleq 2768

This theorem is referenced by:  neeq12i  3030  rabbi  3319  unineq  4140  sbceqg  4245  sbceqi  4246  preq2b  4650  preqr2  4652  otth  5230  otthg  5231  rncoeq  5685  fresaunres1  6378  eqfnov  7094  mpo2eqb  7097  f1o2ndf1  7620  wfrlem5  7760  ecopovsym  8195  karden  9114  adderpqlem  10170  mulerpqlem  10171  addcmpblnr  10285  ax1ne0  10376  addid1  10616  sq11i  13366  nn0opth2i  13443  oppgcntz  18257  islpir  19737  evlsval  20006  volfiniun  23845  dvmptfsum  24269  axlowdimlem13  26437  usgredg2v  26706  issubgr  26750  clwlkcompbp  27265  pjneli  29275  madjusmdetlem1  30725  breprexp  31543  bnj553  31808  bnj1253  31925  fprlem1  32628  frrlem15  32633  sltval2  32654  sltsolem1  32671  nosepnelem  32675  nolt02o  32690  altopthsn  32913  bj-2upleq  33807  relowlpssretop  34052  iscrngo2  34695  extid  34990  cdleme18d  36854  fphpd  38787  rp-fakeuninass  39256  relexp0eq  39387  comptiunov2i  39392  clsk1indlem1  39736  ntrclskb  39760  onfrALTlem5  40272  onfrALTlem4  40273  onfrALTlem5VD  40615  onfrALTlem4VD  40616  dvnprodlem3  41642  sge0xadd  42127  reuabaiotaiota  42672  rrx2linest  44071