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  3455  relop  4778  csbcnvg  4812  dfiun3g  4885  dfiin3g  4886  resima2  4942  relcnvfld  5163  uniabio  5189  fntpg  5273  dffn5im  5562  dfimafn2  5566  fncnvima2  5638  fmptcof  5684  fcoconst  5688  fnasrng  5697  ffnov  5979  fnovim  5983  fnrnov  6020  foov  6021  funimassov  6024  ovelimab  6025  ofc12  6103  caofinvl  6105  dftpos3  6263  tfr0dm  6323  rdgisucinc  6386  oasuc  6465  ecinxp  6610  phplem1  6852  exmidpw  6908  exmidpweq  6909  unfiin  6925  fidcenumlemr  6954  0ct  7106  ctmlemr  7107  exmidaclem  7207  indpi  7341  nqnq0pi  7437  nq0m0r  7455  addnqpr1  7561  recexgt0sr  7772  suplocsrlempr  7806  recidpipr  7855  recidpirq  7857  axrnegex  7878  nntopi  7893  cnref1o  9650  fztp  10078  fseq1m1p1  10095  fz0to4untppr  10124  frecuzrdgrrn  10408  frecuzrdgsuc  10414  frecuzrdgsuctlem  10423  seq3val  10458  seqvalcd  10459  fser0const  10516  mulexpzap  10560  expaddzap  10564  bcp1m1  10745  cjexp  10902  rexuz3  10999  bdtri  11248  climconst  11298  sumfct  11382  zsumdc  11392  fsum3  11395  sum0  11396  fsumcnv  11445  mertenslem2  11544  zproddc  11587  fprodseq  11591  prod0  11593  prod1dc  11594  prodfct  11595  fprodcnv  11633  ef0lem  11668  efzval  11691  efival  11740  sinbnd  11760  cosbnd  11761  eucalgval  12054  eucalginv  12056  eucalglt  12057  eucalgcvga  12058  eucalg  12059  sqpweven  12175  2sqpwodd  12176  dfphi2  12220  phimullem  12225  prmdiv  12235  odzval  12241  pcval  12296  pczpre  12297  pcrec  12308  ennnfonelemhdmp1  12410  ennnfonelemkh  12413  ressinbasd  12533  topnvalg  12700  imasival  12727  imasplusg  12729  qusval  12744  xpsval  12771  ismgm  12776  plusffvalg  12781  grpidvalg  12792  issgrp  12809  ismnddef  12819  ismhm  12853  isgrp  12883  grpn0  12908  grpinvfvalg  12915  grpsubfvalg  12918  mulgfvalg  12985  mulgval  12986  mulgnn0p1  12994  issubg  13033  isnsg  13062  eqgfval  13081  iscmn  13096  mgpvalg  13133  issrg  13148  isring  13183  iscrng  13186  opprvalg  13241  isnzr  13325  islring  13333  issubrg  13342  islmod  13381  scaffvalg  13396  istps  13535  cldval  13602  ntrfval  13603  clsfval  13604  neifval  13643  restbasg  13671  tgrest  13672  txval  13758  upxp  13775  uptx  13777  txrest  13779  lmcn2  13783  cnmpt2t  13796  cnmpt2res  13800  imasnopn  13802  psmetxrge0  13835  xmetge0  13868  isxms  13954  isms  13956  bdxmet  14004  qtopbasss  14024  cnblcld  14038  negfcncf  14092  dvfvalap  14153  eldvap  14154  dvidlemap  14163  dvexp2  14179  dvrecap  14180  dveflem  14190  sin0pilem1  14205  ptolemy  14248  coskpi  14272  logbrec  14381  lgslem1  14404  lgsval  14408  lgsval4  14424  lgsfcl3  14425  lgsdilem  14431  lgsdir2lem4  14435  lgsdir2lem5  14436  nninfsellemqall  14767