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 1569

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1809  df-cleq 2754

This theorem is used by:  neeq12i  3023  rabbi  3445  unineq  4240  vn0  4297  vn0OLD  4298  sbceqg  4376  sbceqi  4377  preq2b  4811  preqr2  4813  otth  5465  otthg  5466  rncoeq  5970  fresaunres1  6751  eqfnov  7541  mpo2eqb  7544  f1o2ndf1  8115  fprlem1  8295  ecopovsym  8815  frrlem15  9727  kardenOLD  9887  adderpqlem  10945  mulerpqlem  10946  addcmpblnr  11060  ax1ne0  11151  addrid  11396  sq11i  14234  nn0opth2i  14314  oppgcntz  19440  opprdomnb  20826  isdomn4r  20828  islpir  21507  evlsval  22248  volfiniun  25717  dvmptfsum  26145  ltsval2  27831  ltssolem1  27850  nosepnelem  27854  nolt02o  27870  axlowdimlem13  29315  usgredg2v  29588  issubgr  29632  clwlkcompbp  30142  pjneli  32086  indifbi  32877  madjusmdetlem1  34226  breprexp  35029  bnj553  35295  bnj1253  35414  gonanegoal  35852  goalrlem  35896  goalr  35897  fmlasucdisj  35899  satffunlem  35901  satffunlem1lem1  35902  satffunlem2lem1  35904  altopthsn  36461  bj-2upleq  37676  bj-vn0ALT  37736  relowlpssretop  38038  iscrngo2  38676  extid  38993  cdleme18d  41097  fphpd  43571  oenassex  44073  rp-fakeuninass  44270  relexp0eq  44455  comptiunov2i  44460  clsk1indlem1  44799  ntrclskb  44823  onfrALTlem5  45279  onfrALTlem4  45280  onfrALTlem5VD  45621  onfrALTlem4VD  45622  dvnprodlem3  46690  sge0xadd  47177  reuabaiotaiota  47852  rrx2linest  49550  fucofvalne  50131