MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqeq12i Structured version   Visualization version   GIF version

Theorem eqeq12i 2836
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
StepHypRef Expression
1 eqeq12i.1 . . 3 𝐴 = 𝐵
21eqeq1i 2826 . 2 (𝐴 = 𝐶𝐵 = 𝐶)
3 eqeq12i.2 . . 3 𝐶 = 𝐷
43eqeq2i 2834 . 2 (𝐵 = 𝐶𝐵 = 𝐷)
52, 4bitri 276 1 (𝐴 = 𝐶𝐵 = 𝐷)
Colors of variables: wff setvar class
Syntax hints:  wb 207   = wceq 1528
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-9 2115  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2814
This theorem is referenced by:  neeq12i  3082  rabbi  3384  unineq  4253  sbceqg  4360  sbceqi  4361  preq2b  4772  preqr2  4774  otth  5368  otthg  5369  rncoeq  5840  fresaunres1  6545  eqfnov  7269  mpo2eqb  7272  f1o2ndf1  7809  wfrlem5  7950  ecopovsym  8389  karden  9313  adderpqlem  10365  mulerpqlem  10366  addcmpblnr  10480  ax1ne0  10571  addid1  10809  sq11i  13544  nn0opth2i  13621  oppgcntz  18432  islpir  19952  evlsval  20229  volfiniun  24077  dvmptfsum  24501  axlowdimlem13  26668  usgredg2v  26937  issubgr  26981  clwlkcompbp  27491  pjneli  29428  madjusmdetlem1  30992  breprexp  31804  bnj553  32070  bnj1253  32187  gonanegoal  32497  goalrlem  32541  goalr  32542  fmlasucdisj  32544  satffunlem  32546  satffunlem1lem1  32547  satffunlem2lem1  32549  fprlem1  33035  frrlem15  33040  sltval2  33061  sltsolem1  33078  nosepnelem  33082  nolt02o  33097  altopthsn  33320  bj-2upleq  34222  relowlpssretop  34528  iscrngo2  35158  extid  35451  cdleme18d  37313  fphpd  39293  rp-fakeuninass  39762  relexp0eq  39926  comptiunov2i  39931  clsk1indlem1  40275  ntrclskb  40299  onfrALTlem5  40756  onfrALTlem4  40757  onfrALTlem5VD  41099  onfrALTlem4VD  41100  dvnprodlem3  42113  sge0xadd  42598  reuabaiotaiota  43168  rrx2linest  44627
  Copyright terms: Public domain W3C validator