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  7448  ctmlemr  7449  exmidaclem  7565  pw1m  7584  indpi  7710  nqnq0pi  7806  nq0m0r  7824  addnqpr1  7930  recexgt0sr  8141  suplocsrlempr  8175  recidpipr  8224  recidpirq  8226  axrnegex  8247  nntopi  8262  fcdmnn0supp  9620  fcdmnn0suppg  9622  cnref1o  10062  fztp  10496  fseq1m1p1  10513  fz0to4untppr  10542  frecuzrdgrrn  10860  frecuzrdgsuc  10866  frecuzrdgsuctlem  10875  seq3val  10912  seqvalcd  10913  fser0const  10987  mulexpzap  11031  expaddzap  11035  bcp1m1  11219  hashfibclem  11298  hash2en  11311  iswrdiz  11327  pfxccatin12lem2c  11518  cjexp  11674  rexuz3  11772  bdtri  12025  climconst  12075  sumfct  12159  zsumdc  12170  fsum3  12173  sum0  12174  fsumcnv  12223  mertenslem2  12322  zproddc  12365  fprodseq  12369  prod0  12371  prod1dc  12372  prodfct  12373  fprodcnv  12411  ef0lem  12446  efzval  12469  efival  12518  sinbnd  12538  cosbnd  12539  eucalgval  12851  eucalginv  12853  eucalglt  12854  eucalgcvga  12855  eucalg  12856  sqpweven  12974  2sqpwodd  12975  dfphi2  13021  phimullem  13026  prmdiv  13036  odzval  13043  pcval  13098  pczpre  13099  pcrec  13110  4sqlem17  13209  ballotfilemimin  13301  ennnfonelemhdmp1  13352  ennnfonelemkh  13355  ressinbasd  13481  restid2  13655  topnvalg  13658  imasival  13680  imasplusg  13682  qusval  13697  ismgm  13730  plusffvalg  13735  grpidvalg  13746  gzsumvalx  13762  issgrp  13771  ismnddef  13784  ismhm  13821  isgrp  13864  grpn0  13893  grpinvfvalg  13900  grpsubfvalg  13903  mulgfvalg  13977  mulgval  13978  mulgnn0p1  13989  issubg  14029  isnsg  14058  eqgfval  14078  quseccl0g  14087  isghm  14099  conjsubg  14133  conjsubgen  14134  cntrval  14145  cntzfval  14146  iscmn  14180  gsumclfi  14243  gsumf1ofi  14244  gsummptfidmadd  14245  prdsval  14257  prdsbas3  14271  xpsval  14285  pwsval  14288  pwsbas  14289  pwselbasb  14290  pwsplusgval  14292  pwsmulrval  14293  pws0g  14297  pwsinvg  14299  mgpvalg  14304  isrng  14317  issrg  14353  isring  14388  iscrng  14391  opprvalg  14458  dfrhm2  14545  isnzr  14572  islring  14583  issubrg  14613  rrgval  14654  isdomn  14662  isdrngtap  14690  islmod  14711  scaffvalg  14727  lsssetm  14777  lspfval  14809  2idlval  14923  2idlvalg  14924  mulgrhm2  15029  zlmval  15046  znval  15055  znzrhfo  15067  znle2  15071  aspval  15099  asclfval  15105  psrval  15134  mplvalcoe  15172  istps  15224  cldval  15291  ntrfval  15292  clsfval  15293  neifval  15332  restbasg  15360  tgrest  15361  txval  15447  upxp  15464  uptx  15466  txrest  15468  lmcn2  15472  cnmpt2t  15485  cnmpt2res  15489  imasnopn  15491  psmetxrge0  15524  xmetge0  15557  isxms  15643  isms  15645  bdxmet  15693  qtopbasss  15713  cnblcld  15727  mpomulcn  15758  negfcncf  15798  dvfvalap  15873  eldvap  15874  dvidlemap  15883  dvidrelem  15884  dvidsslem  15885  dvexp2  15904  dvrecap  15905  dveflem  15918  plyconst  15937  plycolemc  15950  sin0pilem1  15974  ptolemy  16017  coskpi  16041  logbrec  16157  zprmlogbaplem3  16178  birthdaylem2  16187  prmorcht  16243  mpodvdsmulf1o  16245  fsumdvdsmul  16246  ppiqub  16254  bposlem8  16279  lgslem1  16285  lgsval  16289  lgsval4  16305  lgsfcl3  16306  lgsdilem  16312  lgsdir2lem4  16316  lgsdir2lem5  16317  gausslemma2dlem5  16351  lgsquadlem2  16363  iedgedgg  16468  isuhgrm  16478  isushgrm  16479  isupgren  16502  isumgren  16512  isuspgren  16564  isusgren  16565  usgrstrrepeen  16638  vtxdgfval  16695  wksfval  16729  ifpsnprss  16750  clwwlkg  16800  clwwlkn1  16825  eupthsg  16852  eupth2fi  16886  nninfsellemqall  17224  qdiff  17265