Theorem eqtr4di 2289

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 2242	. 2 |- B = C
4	1, 3	eqtrdi 2287	1 |- ( ph -> A = C )

This proof depends on syntax axioms:   -> wi 4   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  3eqtr4g  2296  rabxmdc  3554  ifpprsnssdc  3820  relop  4930  csbcnvg  4964  dfiun3g  5039  dfiin3g  5040  resima2  5097  relcnvfld  5321  uniabio  5348  fntpg  5437  dffn5im  5748  dfimafn2  5752  fncnvima2  5830  fmptcof  5875  fcoconst  5879  fnasrng  5889  funopsn  5891  fncofn  5893  ffnov  6192  fnovim  6197  fnrnov  6235  foov  6236  funimassov  6239  ovelimab  6240  ofc12  6326  caofinvl  6328  dftpos3  6533  tfr0dm  6593  rdgisucinc  6656  oasuc  6737  ecinxp  6884  mapunen  7151  phplem1  7153  exmidpw  7215  exmidpweq  7216  unfiin  7233  fidcenumlemr  7272  0ct  7447  ctmlemr  7448  exmidaclem  7564  pw1m  7583  indpi  7709  nqnq0pi  7805  nq0m0r  7823  addnqpr1  7929  recexgt0sr  8140  suplocsrlempr  8174  recidpipr  8223  recidpirq  8225  axrnegex  8246  nntopi  8261  fcdmnn0supp  9619  fcdmnn0suppg  9621  cnref1o  10061  fztp  10495  fseq1m1p1  10512  fz0to4untppr  10541  frecuzrdgrrn  10858  frecuzrdgsuc  10864  frecuzrdgsuctlem  10873  seq3val  10910  seqvalcd  10911  fser0const  10985  mulexpzap  11029  expaddzap  11033  bcp1m1  11217  hashfibclem  11296  hash2en  11309  iswrdiz  11325  pfxccatin12lem2c  11516  cjexp  11672  rexuz3  11770  bdtri  12022  climconst  12072  sumfct  12156  zsumdc  12167  fsum3  12170  sum0  12171  fsumcnv  12220  mertenslem2  12319  zproddc  12362  fprodseq  12366  prod0  12368  prod1dc  12369  prodfct  12370  fprodcnv  12408  ef0lem  12443  efzval  12466  efival  12515  sinbnd  12535  cosbnd  12536  eucalgval  12848  eucalginv  12850  eucalglt  12851  eucalgcvga  12852  eucalg  12853  sqpweven  12971  2sqpwodd  12972  dfphi2  13018  phimullem  13023  prmdiv  13033  odzval  13040  pcval  13095  pczpre  13096  pcrec  13107  4sqlem17  13206  ballotfilemimin  13298  ennnfonelemhdmp1  13349  ennnfonelemkh  13352  ressinbasd  13477  restid2  13651  topnvalg  13654  imasival  13676  imasplusg  13678  qusval  13693  ismgm  13726  plusffvalg  13731  grpidvalg  13742  gzsumvalx  13758  issgrp  13767  ismnddef  13780  ismhm  13817  isgrp  13860  grpn0  13889  grpinvfvalg  13896  grpsubfvalg  13899  mulgfvalg  13973  mulgval  13974  mulgnn0p1  13985  issubg  14025  isnsg  14054  eqgfval  14074  quseccl0g  14083  isghm  14095  conjsubg  14129  conjsubgen  14130  iscmn  14145  gsumclfi  14208  gsumf1ofi  14209  gsummptfidmadd  14210  prdsval  14222  prdsbas3  14236  xpsval  14250  pwsval  14253  pwsbas  14254  pwselbasb  14255  pwsplusgval  14257  pwsmulrval  14258  pws0g  14262  pwsinvg  14264  mgpvalg  14269  isrng  14282  issrg  14318  isring  14353  iscrng  14356  opprvalg  14423  dfrhm2  14510  isnzr  14537  islring  14548  issubrg  14578  rrgval  14619  isdomn  14627  isdrngtap  14655  islmod  14676  scaffvalg  14692  lsssetm  14742  lspfval  14774  2idlval  14888  2idlvalg  14889  mulgrhm2  14994  zlmval  15011  znval  15020  znzrhfo  15032  znle2  15036  aspval  15064  asclfval  15070  psrval  15099  mplvalcoe  15130  istps  15182  cldval  15249  ntrfval  15250  clsfval  15251  neifval  15290  restbasg  15318  tgrest  15319  txval  15405  upxp  15422  uptx  15424  txrest  15426  lmcn2  15430  cnmpt2t  15443  cnmpt2res  15447  imasnopn  15449  psmetxrge0  15482  xmetge0  15515  isxms  15601  isms  15603  bdxmet  15651  qtopbasss  15671  cnblcld  15685  mpomulcn  15716  negfcncf  15756  dvfvalap  15831  eldvap  15832  dvidlemap  15841  dvidrelem  15842  dvidsslem  15843  dvexp2  15862  dvrecap  15863  dveflem  15876  plyconst  15895  plycolemc  15908  sin0pilem1  15932  ptolemy  15975  coskpi  15999  logbrec  16115  zprmlogbaplem3  16136  birthdaylem2  16145  mpodvdsmulf1o  16185  fsumdvdsmul  16186  ppiqub  16194  lgslem1  16217  lgsval  16221  lgsval4  16237  lgsfcl3  16238  lgsdilem  16244  lgsdir2lem4  16248  lgsdir2lem5  16249  gausslemma2dlem5  16283  lgsquadlem2  16295  iedgedgg  16400  isuhgrm  16410  isushgrm  16411  isupgren  16434  isumgren  16444  isuspgren  16496  isusgren  16497  usgrstrrepeen  16570  vtxdgfval  16627  wksfval  16661  ifpsnprss  16682  clwwlkg  16732  clwwlkn1  16757  eupthsg  16784  eupth2fi  16818  nninfsellemqall  17156  qdiff  17196