Theorem eqtr 1119

Description: An equality transitivity inference.

Hypotheses

Ref	Expression
eqtr.1	|- A = B
eqtr.2	|- B = C

Assertion

Ref	Expression
eqtr	|- A = C

Proof of Theorem eqtr

Step	Hyp	Ref	Expression
1		eqtr.1	. 2 |- A = B
2		eqtr.2	. . 3 |- B = C
3	2	cleq2i 1111	. 2 |- (A = B <-> A = C)
4	1, 3	mpbi 164	1 |- A = C

Syntax hints:   = wceq 1091

This theorem is referenced by:  eqtr2 1120  eqtr3 1121  eqtr4 1122  3eqtr 1123  3eqtr3 1124  3eqtr4 1126  rabab 1359  difeq12i 1586  uneq12i 1609  ineq12i 1643  dfun3 1671  dfin3 1672  invdif 1674  indif 1675  difundi 1681  difindi 1683  symdif1 1689  unrab 1694  undif1 1761  dfpr2 1821  dfuni2 1921  intmin2 1984  op1stb 1992  intunsn 1993  unopab 2121  supex 2157  dfepfr 2184  orddif 2326  onuninsuc 2356  fconstopab 2448  dfdm3 2522  dfrn3 2524  dmopab 2539  dmopab2 2541  rnopab 2566  rnco 2571  rncoeq 2574  resundi 2582  resabs1 2592  resabs2 2593  resopab 2598  dfima3 2605  ndmima 2623  op1sta 2635  rnsnop 2637  op2ndb 2638  op2nda 2639  rnun 2644  imaun 2647  rnxp 2657  funi 2692  funcnvuni 2706  funcnvres 2710  fnresdisj 2732  fconst 2774  fv2 2828  abrexexlem2 2911  tfrlem3 2951  tfrlem8 2956  tfrlem9 2957  tfrlem10 2958  tz7.44-2 2967  rdglem1 2975  rdgsucopabn 2985  abianfplem 2999  opreq12i 3011  fnoprab 3038  oprabval 3047  oprabvalig 3048  caopr31 3076  caopr42 3080  caoprdilem 3082  caoprmo 3084  op1st 3091  op2nd 3092  df1o2 3111  ecidsn 3224  oprec 3254  fnmap 3262  mapvalg 3263  xpassen 3344  sbthlem5 3353  sbthlem8 3356  mapunen 3397  ssenen 3399  limensuci 3401  phplem2 3404  inf3lema 3460  inf3lemb 3461  trcl 3489  zfregs 3491  r10 3495  unir1 3511  rankval 3512  kardex 3550  aceq3 3556  ac6lem 3575  kmlem10 3589  kmlem11 3590  zornlem1 3603  fodomb 3615  hta 3619  aleph0 3669  cf0 3705  cdavalt 3716  cdaassen 3725  addpiord 3806  mulpiord 3807  dmaddpi 3812  dmmulpi 3813  addcmpblnq 3846  addcompq 3856  dmrecpq 3868  ltapq 3870  ltmpq 3871  1lt2pq 3872  ltaddpq 3873  mulcomsr 3992  distrsr 3994  ltasr 4003  recexsrlem 4006  sqgt0sr 4009  map2psrpr 4014  supsrlem4 4022  supsrlem5 4023  addcnsr 4047  mulcnsr 4048  mulresr 4051  axaddex 4059  axmulex 4060  axmulcom 4071  axmulass 4073  axdistr 4074  axrecex 4079  axi2m1 4082  axcnre 4087  addid2 4113  mulid2 4115  add42 4131  negid 4147  subneg 4148  subid 4155  subeq0 4163  neg0 4170  mulzer2 4186  1p1times 4187  mul2neg 4192  negdi 4193  divcan1 4225  divrec 4236  divcan3 4247  divcan4 4248  divid 4254  divzer 4255  ltadd2 4312  ltsubadd 4316  recgt0i 4385  2times 4489  times2 4491  2t2e4 4503  3t2e6 4504  3t3e9 4505  4t2e8 4506  crulem 4528  uzwo3lem2 4615  om2uz0 4651  uzrdgini 4658  seqlem1 4662  seqrval 4664  seqval 4665  sqreci 4690  sq1 4709  sq2 4710  cu2 4711  binom 4712  discrlem1 4713  nneo 4719  nn0opthlem1 4722  sqrlem2 4732  sqrlem10 4740  sqrlem11 4741  sqrlem16 4746  sqrth 4757  sqr2irrlem1 4777  cjcj 4808  cjre 4811  recj 4812  imcj 4813  readd 4814  imadd 4815  remul 4816  immul 4817  cjadd 4818  cjmul 4819  reneg 4824  imneg 4826  cjneg 4827  addcj 4828  absval2 4836  absvalsq 4837  absvalsq2 4838  abs00 4839  absneg 4843  absmul 4846  sqabsadd 4847  absid 4850  releabs 4858  abstri 4859  facnnt 4870  fac1 4872  facp1t 4873  ruclem2 4886  ruclem3 4887  ruclem7 4891  ruclem14 4898  ruclem15 4899  infxpidmlem6 4938  infxpidmlem11 4943  infmap2lem1 4951  hv2neg 5010  hvsubdistr1 5024  hvsubass 5027  hv2times 5033  hvnegdi 5034  hvsubeq0 5035  hvsubcan2 5036  normlem0 5062  normlem1 5063  normlem8 5071  normsq 5082  norm-ii 5086  norm-iii 5087  normsub 5089  norm3dif 5094  normpar 5099  normpar2 5100  bcs 5101  projlem3 5195  projlem4 5196  projlem7 5199  projlem18 5210  pjthlem1 5225  ococ 5252  pjococ 5272  dfchsup2 5299  dfchj2 5325  dfchj3 5326  chdmm2 5399  chdmm3 5400  chdmm4 5401  chdmj2 5403  chdmj3 5404  chdmj4 5405  chjo 5409  h1de2 5458  spanunsn 5482  pjoml3 5496  pjoml4 5497  cmbr2 5505  cmbr3 5509  fh1 5518  fh2 5519  qlax5 5524  qlaxr2 5526  spansnj 5539  pjadj 5564  pjadd 5566  pjmul 5568  pjsub 5569  pjssm 5572  pjdifnorm 5574  pjcj 5575  hoid0r 5615  hosd1 5623  pjpyth 5664  stadd3 5689  cvexch 5760  sumdmd 5787

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