Theorem eqeq12i 2755

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

Syntax hints:   ↔ wb 206   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729

This theorem is referenced by:  neeq12i  2999  rabbi  3420  unineq  4229  vn0  4286  sbceqg  4353  sbceqi  4354  preq2b  4791  preqr2  4793  otth  5433  otthg  5434  rncoeq  5932  fresaunres1  6708  eqfnov  7490  mpo2eqb  7493  f1o2ndf1  8066  fprlem1  8244  ecopovsym  8760  frrlem15  9675  karden  9813  adderpqlem  10871  mulerpqlem  10872  addcmpblnr  10986  ax1ne0  11077  addrid  11320  sq11i  14147  nn0opth2i  14227  oppgcntz  19333  opprdomnb  20688  isdomn4r  20690  islpir  21321  evlsval  22077  volfiniun  25527  dvmptfsum  25955  ltsval2  27637  ltssolem1  27656  nosepnelem  27660  nolt02o  27676  axlowdimlem13  29040  usgredg2v  29313  issubgr  29357  clwlkcompbp  29868  pjneli  31812  indifbi  32608  madjusmdetlem1  33990  breprexp  34796  bnj553  35059  bnj1253  35178  gonanegoal  35553  goalrlem  35597  goalr  35598  fmlasucdisj  35600  satffunlem  35602  satffunlem1lem1  35603  satffunlem2lem1  35605  altopthsn  36162  bj-2upleq  37338  relowlpssretop  37697  iscrngo2  38335  extid  38654  cdleme18d  40758  fphpd  43265  oenassex  43767  rp-fakeuninass  43964  relexp0eq  44149  comptiunov2i  44154  clsk1indlem1  44493  ntrclskb  44517  onfrALTlem5  44990  onfrALTlem4  44991  onfrALTlem5VD  45332  onfrALTlem4VD  45333  dvnprodlem3  46397  sge0xadd  46884  reuabaiotaiota  47550  rrx2linest  49233  fucofvalne  49815