Theorem eqtr4di 2289

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

Hypotheses

Ref	Expression
eqtr4di.1	⊢ (𝜑 → 𝐴 = 𝐵)
eqtr4di.2	⊢ 𝐶 = 𝐵

Assertion

Ref	Expression
eqtr4di	⊢ (𝜑 → 𝐴 = 𝐶)

Proof of Theorem eqtr4di

Step	Hyp	Ref	Expression
1		eqtr4di.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		eqtr4di.2	. . 3 ⊢ 𝐶 = 𝐵
3	2	eqcomi 2242	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	eqtrdi 2287	1 ⊢ (𝜑 → 𝐴 = 𝐶)

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  9615  fcdmnn0suppg  9617  cnref1o  10051  fztp  10485  fseq1m1p1  10502  fz0to4untppr  10531  frecuzrdgrrn  10845  frecuzrdgsuc  10851  frecuzrdgsuctlem  10860  seq3val  10897  seqvalcd  10898  fser0const  10972  mulexpzap  11016  expaddzap  11020  bcp1m1  11203  hashfibclem  11282  hash2en  11295  iswrdiz  11311  pfxccatin12lem2c  11502  cjexp  11658  rexuz3  11756  bdtri  12006  climconst  12056  sumfct  12140  zsumdc  12151  fsum3  12154  sum0  12155  fsumcnv  12204  mertenslem2  12303  zproddc  12346  fprodseq  12350  prod0  12352  prod1dc  12353  prodfct  12354  fprodcnv  12392  ef0lem  12427  efzval  12450  efival  12499  sinbnd  12519  cosbnd  12520  eucalgval  12832  eucalginv  12834  eucalglt  12835  eucalgcvga  12836  eucalg  12837  sqpweven  12953  2sqpwodd  12954  dfphi2  12998  phimullem  13003  prmdiv  13013  odzval  13020  pcval  13075  pczpre  13076  pcrec  13087  4sqlem17  13186  ballotfilemimin  13249  ennnfonelemhdmp1  13300  ennnfonelemkh  13303  ressinbasd  13428  restid2  13602  topnvalg  13605  imasival  13627  imasplusg  13629  qusval  13644  ismgm  13677  plusffvalg  13682  grpidvalg  13693  gzsumvalx  13709  issgrp  13718  ismnddef  13731  ismhm  13768  isgrp  13811  grpn0  13840  grpinvfvalg  13847  grpsubfvalg  13850  mulgfvalg  13924  mulgval  13925  mulgnn0p1  13936  issubg  13976  isnsg  14005  eqgfval  14025  quseccl0g  14034  isghm  14046  conjsubg  14080  conjsubgen  14081  iscmn  14096  gsumclfi  14159  gsumf1ofi  14160  gsummptfidmadd  14161  prdsval  14173  prdsbas3  14187  xpsval  14201  pwsval  14204  pwsbas  14205  pwselbasb  14206  pwsplusgval  14208  pwsmulrval  14209  pws0g  14213  pwsinvg  14215  mgpvalg  14220  isrng  14233  issrg  14269  isring  14304  iscrng  14307  opprvalg  14374  dfrhm2  14461  isnzr  14488  islring  14499  issubrg  14529  rrgval  14570  isdomn  14578  isdrngtap  14606  islmod  14627  scaffvalg  14643  lsssetm  14693  lspfval  14725  2idlval  14839  2idlvalg  14840  mulgrhm2  14945  zlmval  14962  znval  14971  znzrhfo  14983  znle2  14987  aspval  15015  asclfval  15021  psrval  15050  mplvalcoe  15081  istps  15133  cldval  15200  ntrfval  15201  clsfval  15202  neifval  15241  restbasg  15269  tgrest  15270  txval  15356  upxp  15373  uptx  15375  txrest  15377  lmcn2  15381  cnmpt2t  15394  cnmpt2res  15398  imasnopn  15400  psmetxrge0  15433  xmetge0  15466  isxms  15552  isms  15554  bdxmet  15602  qtopbasss  15622  cnblcld  15636  mpomulcn  15667  negfcncf  15707  dvfvalap  15782  eldvap  15783  dvidlemap  15792  dvidrelem  15793  dvidsslem  15794  dvexp2  15813  dvrecap  15814  dveflem  15827  plyconst  15846  plycolemc  15859  sin0pilem1  15882  ptolemy  15925  coskpi  15949  logbrec  16062  birthdaylem2  16088  mpodvdsmulf1o  16104  fsumdvdsmul  16105  lgslem1  16119  lgsval  16123  lgsval4  16139  lgsfcl3  16140  lgsdilem  16146  lgsdir2lem4  16150  lgsdir2lem5  16151  gausslemma2dlem5  16185  lgsquadlem2  16197  iedgedgg  16302  isuhgrm  16312  isushgrm  16313  isupgren  16336  isumgren  16346  isuspgren  16398  isusgren  16399  usgrstrrepeen  16472  vtxdgfval  16529  wksfval  16563  ifpsnprss  16584  clwwlkg  16634  clwwlkn1  16659  eupthsg  16686  eupth2fi  16720  nninfsellemqall  17058  qdiff  17098