Theorem eqtr4di 2228

Description: An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)

Hypotheses

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

Assertion

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

Proof of Theorem eqtr4di

Step	Hyp	Ref	Expression
1		eqtr4di.1	. 2 |- ( ph -> A = B )
2		eqtr4di.2	. . 3 |- C = B
3	2	eqcomi 2181	. 2 |- B = C
4	1, 3	eqtrdi 2226	1 |- ( ph -> A = C )

Syntax hints:   -> wi 4   = wceq 1353

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170

This theorem is referenced by:  3eqtr4g  2235  rabxmdc  3454  relop  4774  csbcnvg  4808  dfiun3g  4881  dfiin3g  4882  resima2  4938  relcnvfld  5159  uniabio  5185  fntpg  5269  dffn5im  5558  dfimafn2  5562  fncnvima2  5634  fmptcof  5680  fcoconst  5684  fnasrng  5693  ffnov  5974  fnovim  5978  fnrnov  6015  foov  6016  funimassov  6019  ovelimab  6020  ofc12  6098  caofinvl  6100  dftpos3  6258  tfr0dm  6318  rdgisucinc  6381  oasuc  6460  ecinxp  6605  phplem1  6847  exmidpw  6903  exmidpweq  6904  unfiin  6920  fidcenumlemr  6949  0ct  7101  ctmlemr  7102  exmidaclem  7202  indpi  7336  nqnq0pi  7432  nq0m0r  7450  addnqpr1  7556  recexgt0sr  7767  suplocsrlempr  7801  recidpipr  7850  recidpirq  7852  axrnegex  7873  nntopi  7888  cnref1o  9644  fztp  10071  fseq1m1p1  10088  fz0to4untppr  10117  frecuzrdgrrn  10401  frecuzrdgsuc  10407  frecuzrdgsuctlem  10416  seq3val  10451  seqvalcd  10452  fser0const  10509  mulexpzap  10553  expaddzap  10557  bcp1m1  10736  cjexp  10893  rexuz3  10990  bdtri  11239  climconst  11289  sumfct  11373  zsumdc  11383  fsum3  11386  sum0  11387  fsumcnv  11436  mertenslem2  11535  zproddc  11578  fprodseq  11582  prod0  11584  prod1dc  11585  prodfct  11586  fprodcnv  11624  ef0lem  11659  efzval  11682  efival  11731  sinbnd  11751  cosbnd  11752  eucalgval  12044  eucalginv  12046  eucalglt  12047  eucalgcvga  12048  eucalg  12049  sqpweven  12165  2sqpwodd  12166  dfphi2  12210  phimullem  12215  prmdiv  12225  odzval  12231  pcval  12286  pczpre  12287  pcrec  12298  ennnfonelemhdmp1  12400  ennnfonelemkh  12403  ressinbasd  12523  topnvalg  12686  ismgm  12706  plusffvalg  12711  grpidvalg  12722  issgrp  12739  ismnddef  12749  ismhm  12781  isgrp  12811  grpn0  12836  grpinvfvalg  12843  grpsubfvalg  12846  mulgfvalg  12913  mulgval  12914  mulgnn0p1  12922  issubg  12960  iscmn  12996  mgpvalg  13033  issrg  13048  isring  13083  iscrng  13086  opprvalg  13140  isnzr  13224  islring  13232  istps  13312  cldval  13381  ntrfval  13382  clsfval  13383  neifval  13422  restbasg  13450  tgrest  13451  txval  13537  upxp  13554  uptx  13556  txrest  13558  lmcn2  13562  cnmpt2t  13575  cnmpt2res  13579  imasnopn  13581  psmetxrge0  13614  xmetge0  13647  isxms  13733  isms  13735  bdxmet  13783  qtopbasss  13803  cnblcld  13817  negfcncf  13871  dvfvalap  13932  eldvap  13933  dvidlemap  13942  dvexp2  13958  dvrecap  13959  dveflem  13969  sin0pilem1  13984  ptolemy  14027  coskpi  14051  logbrec  14160  lgslem1  14183  lgsval  14187  lgsval4  14203  lgsfcl3  14204  lgsdilem  14210  lgsdir2lem4  14214  lgsdir2lem5  14215  nninfsellemqall  14535