Theorem cleq12d 1115

Description: A useful inference for substituting definitions into an equality.

Hypotheses

Ref	Expression
cleq12d.1	⊢ (φ → A = B)
cleq12d.2	⊢ (φ → C = D)

Assertion

Ref	Expression
cleq12d	⊢ (φ → (A = C ↔ B = D))

Proof of Theorem cleq12d

Step	Hyp	Ref	Expression
1		cleq12d.1	. . 3 ⊢ (φ → A = B)
2	1	cleq1d 1109	. 2 ⊢ (φ → (A = C ↔ B = C))
3		cleq12d.2	. . 3 ⊢ (φ → C = D)
4	3	cleq2d 1112	. 2 ⊢ (φ → (B = C ↔ B = D))
5	2, 4	bitrd 406	1 ⊢ (φ → (A = C ↔ B = D))

Syntax hints:   → wi 2   ↔ wb 127   = wceq 1091

This theorem is referenced by:  cleqan12d 1116  unisng 1933  ordunisuc 2339  unizlim 2364  orduninsuc 2365  fveqres 2851  cleqfvf 2881  fvreseq 2882  fnressn 2897  fvi 2900  tfrlem1 2949  tfrlem2 2950  tfrlem3 2951  tfrlem9 2957  tfrlem10 2958  tfrlem11 2959  tfrlem12 2960  tfr2 2963  tfr3 2964  tz7.44-1 2966  tz7.44-2 2967  tz7.44-3 2968  rdglem1 2975  rdgzert 2982  rdgsuct 2983  rdglimt 2986  abianfp 3000  caoprcom 3067  caoprass 3068  caoprcan 3069  caoprdistr 3073  caoprmo 3084  1st2val 3097  df1st2 3098  oalim 3135  omlim 3136  oelim 3137  oa0r 3141  om0r 3142  om1r 3145  oaass 3163  nnacom 3175  nndi 3180  nnmass 3181  nnmsucr 3182  nnmcom 3183  ecoprcom 3255  ecoprass 3256  ecoprdi 3257  dom2d 3307  rankvalg 3513  rankonid 3538  rankr1id 3539  carduni 3664  cardprc 3667  alephcard 3673  cardalephex 3691  cardcf 3706  mulcanpi 3821  mulidpq 3863  genpv 3896  0idsr 4000  1idsr 4001  supsrlem2 4020  ax0id 4076  ax1id 4077  addcan 4120  addcant 4122  addcan2t 4123  subnegt 4149  negnegt 4157  subid1t 4160  subdit 4184  mulneg1t 4196  mul2negt 4199  negdit 4200  mulcan 4207  mulcant 4208  mulcant2 4209  divcan1t 4228  divcan2t 4229  divrecz 4237  divrect 4238  divdistrz 4245  divdistrt 4246  divcan3t 4251  div1t 4258  recrect 4260  eqneg 4378  2timest 4490  om2uzsuc 4652  seqlem1 4662  expaddt 4698  nneo 4719  sqrth 4757  sqrmul 4763  sqsqrt 4776  cjret 4829  cjcjt 4830  cjaddt 4831  cjmult 4832  absmult 4849  absidt 4862  abssubt 4864  abslem2 4867  hvsubsub4t 5032  hvnegdit 5039  hiidrclt 5053  hial2eqt 5060  norm-iiit 5088  normsubt 5091  normpytht 5092  chocuni 5179  pjthlem8 5232  ococt 5253  axpjpjt 5260  chj0t 5414  chlejb1t 5429  chdmm1t 5438  chjasst 5446  spansnt 5464  elspansn2t 5472  cmbrt 5494  pjoml3t 5517  spansnjt 5540  pjch1t 5560  pjadjt 5576  pjaddt 5577  pjsubt 5578  pjmult 5579  pjcjt2 5580  pjcht 5582  pjss2co 5634  pjssmt 5635  pjssge0t 5636  pjopytht 5662  stelt 5671  stjt 5676  mdbr 5726  mdi 5727  mdbr3 5729  dmdbr 5731  dmdi 5732

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-gen 677  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-cleq 1097

metamath.org