Theorem eqtr4d 1502

Description: An equality transitivity equality deduction.

Hypotheses

Ref	Expression
eqtr4d.1	|- (ph -> A = B)
eqtr4d.2	|- (ph -> C = B)

Assertion

Ref	Expression
eqtr4d	|- (ph -> A = C)

Proof of Theorem eqtr4d

Step	Hyp	Ref	Expression
1		eqtr4d.1	. 2 |- (ph -> A = B)
2		eqtr4d.2	. . 3 |- (ph -> C = B)
3	2	eqcomd 1472	. 2 |- (ph -> B = C)
4	1, 3	eqtrd 1499	1 |- (ph -> A = C)

Syntax hints:   -> wi 3   = wceq 953

This theorem is referenced by:  3eqtr2d 1505  3eqtr2rd 1506  3eqtr4d 1509  3eqtr4rd 1510  ifswap 2372  opthwiener 2796  relop 3265  relimasn 3409  f1ococnv2 3693  fveqres 3734  funfv 3755  fvco 3759  fsn2 3821  fconst2g 3830  ndmoprcom 4033  ndmoprass 4034  ndmoprdistr 4035  1stval 4065  2ndval 4066  1st2val 4079  2nd2val 4080  curry1val 4084  oev2 4146  oesuc 4150  oaass 4179  odi 4194  omass 4195  oewordi 4202  oewordri 4203  oelim2 4206  nnacom 4217  nnmsucr 4224  nnmcom 4225  fundmen 4409  pw2en 4426  xpmapenlem3 4478  ranklim 4657  rankuni 4670  cardval 4798  cfsuc 4887  distrpq 5039  recmulpq 5042  addcompr 5095  mulcompr 5097  mulcmpblnrlem 5154  0idsr 5178  1idsr 5179  cnegext 5320  mulneg12t 5425  subsub3t 5435  subadd4t 5447  mulsubt 5449  recextlem1 5655  halfaddsubt 5988  supxrre 6030  zaddclt 6112  uzrdgsuc 6241  shftval2t 6284  shftval4t 6286  seqzfval2 6470  seq1seq0 6477  mulexpt 6525  recexpt 6526  expaddt 6527  expmult 6528  divexpt 6530  expword2it 6536  subsqt 6573  bernneq 6583  nn0opth 6596  imret 6710  cjexpt 6752  abscjt 6769  absret 6801  abs1m 6841  caure 6864  cauim 6865  facp1t 6873  faclbnd 6882  faclbnd6 6891  bccmplt 6900  sumeq2 6923  fsum1ps 6956  fsumsplit 6958  fsumconst 6976  serzmulc1 6995  binomlem2 7005  iserzshft2 7044  climrecl 7047  climaddc1 7054  climsub 7066  climsubc2 7067  caucvg3a 7100  caucvg3lem 7102  ser1cmp2 7113  iserzabslem 7114  isumshft 7139  isumshft2 7140  isummulc1ALT 7148  infcvglem2 7157  geolimilem 7170  0.999... 7181  cvgratlem2ALT 7183  cvgratlem2 7186  negfcncf 7204  mulc1cncf 7214  efcltlem1 7246  dfef2 7249  erelem2 7262  efaddlem26 7305  efsubt 7313  ef1tllem 7323  ef01tllem1 7325  eirrlem2 7331  efi4pt 7377  sinnegt 7384  efeult 7391  subcost 7402  sincossqt 7403  cos2tt 7405  demoivre 7426  iscncl 7709  ioo2bl 7851  xplmi 7907  fsumcnlem 7923  bcthlem1 7933  grpidinv2 7994  grpinv 8003  grp2inv 8013  grpinvf 8014  grpinvdiv 8019  grpsn 8061  ablsn 8062  ghgrpilem1 8070  ghsubgi 8075  ringsn 8100  vcoprne 8136  bafval 8161  nvmfval 8204  nvge0 8241  imsmetlem 8261  ipval2 8291  ipval3 8293  ip0r 8304  ip1cnilem6 8312  sspmlem 8325  lnocoi 8352  nvcnpi4 8355  nmlno0lem 8385  blometi 8394  ipasslem1 8421  ipasslem11 8431  ipblnfi 8447  minveclem9 8484  minveclem18 8493  minveclem19 8494  minveclem30 8505  minveclem35 8510  minveclem36 8511  minveclem38 8513  sinco 8586  cosco 8587  sinperlem1 8605  efimpi 8615  shftefif1olem 8661  shftefif1olemOLD 8662  hvsub4t 8827  hvsubdistr2t 8838  his5t 8874  hhip 8965  pjpot 9176  shscl 9196  hsupvalt 9216  shjcomt 9245  h1de2b 9392  h1de2bOLD 9393  normcant 9416  spanunsn 9419  cm0t 9469  dfiop2 9596  hocadddir 9622  hocsubdir 9623  honegsub 9639  homco1t 9644  homulasst 9645  hoadddit 9646  hoadddirt 9647  hosubadd4t 9657  eigorth 9680  brafnmult 9791  kbmult 9795  0hmop 9823  0lnfn 9825  adj0 9834  nmlnop0ALT 9835  lnopm 9840  hmopcot 9863  riesz3 9910  cnlnadjlem6 9920  adjlnopt 9934  nmopadjle 9936  adjaddt 9940  nmopco 9942  nmopcoadj 9948  kbass1t 9961  kbass2t 9962  kbass4t 9964  kbass6t 9966  leopsqt 9974  leopnmidt 9982  pjscj 10009  pjinvar 10029  superpos 10189  atord 10219  atcvat3 10231  dmdbr6at 10256  cdj3lem1 10266  ghomsn 10293  hmeogrp 10425  mslb1 10473  cnvtr 10482  cmpassoh 10573  homgrf 10574

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-an 225  df-cleq 1462

Copyright terms: Public domain