Theorem eqtr4di 2282

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 2235	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	eqtrdi 2280	1 ⊢ (𝜑 → 𝐴 = 𝐶)

Syntax hints:   → wi 4   = wceq 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224

This theorem is referenced by:  3eqtr4g  2289  rabxmdc  3526  ifpprsnssdc  3779  relop  4880  csbcnvg  4914  dfiun3g  4989  dfiin3g  4990  resima2  5047  relcnvfld  5270  uniabio  5297  fntpg  5386  dffn5im  5691  dfimafn2  5695  fncnvima2  5768  fmptcof  5814  fcoconst  5818  fnasrng  5828  funopsn  5830  fncofn  5832  ffnov  6125  fnovim  6130  fnrnov  6168  foov  6169  funimassov  6172  ovelimab  6173  ofc12  6259  caofinvl  6261  dftpos3  6428  tfr0dm  6488  rdgisucinc  6551  oasuc  6632  ecinxp  6779  phplem1  7038  exmidpw  7100  exmidpweq  7101  unfiin  7118  fidcenumlemr  7154  0ct  7306  ctmlemr  7307  exmidaclem  7423  pw1m  7442  indpi  7562  nqnq0pi  7658  nq0m0r  7676  addnqpr1  7782  recexgt0sr  7993  suplocsrlempr  8027  recidpipr  8076  recidpirq  8078  axrnegex  8099  nntopi  8114  cnref1o  9885  fztp  10313  fseq1m1p1  10330  fz0to4untppr  10359  frecuzrdgrrn  10671  frecuzrdgsuc  10677  frecuzrdgsuctlem  10686  seq3val  10723  seqvalcd  10724  fser0const  10798  mulexpzap  10842  expaddzap  10846  bcp1m1  11028  hash2en  11108  iswrdiz  11124  pfxccatin12lem2c  11315  cjexp  11471  rexuz3  11568  bdtri  11818  climconst  11868  sumfct  11952  zsumdc  11963  fsum3  11966  sum0  11967  fsumcnv  12016  mertenslem2  12115  zproddc  12158  fprodseq  12162  prod0  12164  prod1dc  12165  prodfct  12166  fprodcnv  12204  ef0lem  12239  efzval  12262  efival  12311  sinbnd  12331  cosbnd  12332  eucalgval  12644  eucalginv  12646  eucalglt  12647  eucalgcvga  12648  eucalg  12649  sqpweven  12765  2sqpwodd  12766  dfphi2  12810  phimullem  12815  prmdiv  12825  odzval  12832  pcval  12887  pczpre  12888  pcrec  12899  4sqlem17  12998  ennnfonelemhdmp1  13048  ennnfonelemkh  13051  ressinbasd  13175  restid2  13349  topnvalg  13352  prdsval  13374  prdsbas3  13388  pwsval  13392  pwsbas  13393  pwselbasb  13394  pwsplusgval  13396  pwsmulrval  13397  imasival  13407  imasplusg  13409  qusval  13424  xpsval  13453  ismgm  13458  plusffvalg  13463  grpidvalg  13474  igsumvalx  13490  issgrp  13504  ismnddef  13519  pws0g  13552  ismhm  13562  isgrp  13607  grpn0  13636  grpinvfvalg  13643  grpsubfvalg  13646  pwsinvg  13713  mulgfvalg  13726  mulgval  13727  mulgnn0p1  13738  issubg  13778  isnsg  13807  eqgfval  13827  quseccl0g  13836  isghm  13848  conjsubg  13882  conjsubgen  13883  iscmn  13898  mgpvalg  13955  isrng  13966  issrg  13997  isring  14032  iscrng  14035  opprvalg  14101  dfrhm2  14187  isnzr  14214  islring  14225  issubrg  14254  rrgval  14295  isdomn  14302  islmod  14324  scaffvalg  14339  lsssetm  14389  lspfval  14421  2idlval  14535  2idlvalg  14536  mulgrhm2  14643  zlmval  14660  znval  14669  znzrhfo  14681  znle2  14685  psrval  14699  mplvalcoe  14723  istps  14775  cldval  14842  ntrfval  14843  clsfval  14844  neifval  14883  restbasg  14911  tgrest  14912  txval  14998  upxp  15015  uptx  15017  txrest  15019  lmcn2  15023  cnmpt2t  15036  cnmpt2res  15040  imasnopn  15042  psmetxrge0  15075  xmetge0  15108  isxms  15194  isms  15196  bdxmet  15244  qtopbasss  15264  cnblcld  15278  mpomulcn  15309  negfcncf  15349  dvfvalap  15424  eldvap  15425  dvidlemap  15434  dvidrelem  15435  dvidsslem  15436  dvexp2  15455  dvrecap  15456  dveflem  15469  plyconst  15488  plycolemc  15501  sin0pilem1  15524  ptolemy  15567  coskpi  15591  logbrec  15703  mpodvdsmulf1o  15733  fsumdvdsmul  15734  lgslem1  15748  lgsval  15752  lgsval4  15768  lgsfcl3  15769  lgsdilem  15775  lgsdir2lem4  15779  lgsdir2lem5  15780  gausslemma2dlem5  15814  lgsquadlem2  15826  iedgedgg  15931  isuhgrm  15941  isushgrm  15942  isupgren  15965  isumgren  15975  isuspgren  16027  isusgren  16028  usgrstrrepeen  16101  vtxdgfval  16158  wksfval  16192  ifpsnprss  16213  clwwlkg  16263  clwwlkn1  16288  eupthsg  16315  eupth2fi  16349  nninfsellemqall  16668  qdiff  16704  gfsumcl  16739