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  3456  relop  4779  csbcnvg  4813  dfiun3g  4886  dfiin3g  4887  resima2  4943  relcnvfld  5164  uniabio  5190  fntpg  5274  dffn5im  5563  dfimafn2  5567  fncnvima2  5639  fmptcof  5685  fcoconst  5689  fnasrng  5698  ffnov  5981  fnovim  5985  fnrnov  6022  foov  6023  funimassov  6026  ovelimab  6027  ofc12  6105  caofinvl  6107  dftpos3  6265  tfr0dm  6325  rdgisucinc  6388  oasuc  6467  ecinxp  6612  phplem1  6854  exmidpw  6910  exmidpweq  6911  unfiin  6927  fidcenumlemr  6956  0ct  7108  ctmlemr  7109  exmidaclem  7209  indpi  7343  nqnq0pi  7439  nq0m0r  7457  addnqpr1  7563  recexgt0sr  7774  suplocsrlempr  7808  recidpipr  7857  recidpirq  7859  axrnegex  7880  nntopi  7895  cnref1o  9652  fztp  10080  fseq1m1p1  10097  fz0to4untppr  10126  frecuzrdgrrn  10410  frecuzrdgsuc  10416  frecuzrdgsuctlem  10425  seq3val  10460  seqvalcd  10461  fser0const  10518  mulexpzap  10562  expaddzap  10566  bcp1m1  10747  cjexp  10904  rexuz3  11001  bdtri  11250  climconst  11300  sumfct  11384  zsumdc  11394  fsum3  11397  sum0  11398  fsumcnv  11447  mertenslem2  11546  zproddc  11589  fprodseq  11593  prod0  11595  prod1dc  11596  prodfct  11597  fprodcnv  11635  ef0lem  11670  efzval  11693  efival  11742  sinbnd  11762  cosbnd  11763  eucalgval  12056  eucalginv  12058  eucalglt  12059  eucalgcvga  12060  eucalg  12061  sqpweven  12177  2sqpwodd  12178  dfphi2  12222  phimullem  12227  prmdiv  12237  odzval  12243  pcval  12298  pczpre  12299  pcrec  12310  ennnfonelemhdmp1  12412  ennnfonelemkh  12415  ressinbasd  12535  topnvalg  12705  imasival  12732  imasplusg  12734  qusval  12749  xpsval  12776  ismgm  12781  plusffvalg  12786  grpidvalg  12797  issgrp  12814  ismnddef  12824  ismhm  12858  isgrp  12888  grpn0  12913  grpinvfvalg  12920  grpsubfvalg  12923  mulgfvalg  12990  mulgval  12991  mulgnn0p1  12999  issubg  13038  isnsg  13067  eqgfval  13086  iscmn  13101  mgpvalg  13138  issrg  13153  isring  13188  iscrng  13191  opprvalg  13246  isnzr  13330  islring  13338  issubrg  13347  islmod  13386  scaffvalg  13401  lsssetm  13449  istps  13571  cldval  13638  ntrfval  13639  clsfval  13640  neifval  13679  restbasg  13707  tgrest  13708  txval  13794  upxp  13811  uptx  13813  txrest  13815  lmcn2  13819  cnmpt2t  13832  cnmpt2res  13836  imasnopn  13838  psmetxrge0  13871  xmetge0  13904  isxms  13990  isms  13992  bdxmet  14040  qtopbasss  14060  cnblcld  14074  negfcncf  14128  dvfvalap  14189  eldvap  14190  dvidlemap  14199  dvexp2  14215  dvrecap  14216  dveflem  14226  sin0pilem1  14241  ptolemy  14284  coskpi  14308  logbrec  14417  lgslem1  14440  lgsval  14444  lgsval4  14460  lgsfcl3  14461  lgsdilem  14467  lgsdir2lem4  14471  lgsdir2lem5  14472  nninfsellemqall  14803