Theorem eqtr4di 2285

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

Syntax hints:   → wi 4   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2216

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

This theorem is referenced by:  3eqtr4g  2292  rabxmdc  3544  ifpprsnssdc  3804  relop  4910  csbcnvg  4944  dfiun3g  5019  dfiin3g  5020  resima2  5077  relcnvfld  5301  uniabio  5328  fntpg  5417  dffn5im  5727  dfimafn2  5731  fncnvima2  5804  fmptcof  5849  fcoconst  5853  fnasrng  5863  funopsn  5865  fncofn  5867  ffnov  6165  fnovim  6170  fnrnov  6208  foov  6209  funimassov  6212  ovelimab  6213  ofc12  6299  caofinvl  6301  dftpos3  6506  tfr0dm  6566  rdgisucinc  6629  oasuc  6710  ecinxp  6857  mapunen  7117  phplem1  7119  exmidpw  7181  exmidpweq  7182  unfiin  7199  fidcenumlemr  7238  0ct  7411  ctmlemr  7412  exmidaclem  7528  pw1m  7547  indpi  7673  nqnq0pi  7769  nq0m0r  7787  addnqpr1  7893  recexgt0sr  8104  suplocsrlempr  8138  recidpipr  8187  recidpirq  8189  axrnegex  8210  nntopi  8225  fcdmnn0supp  9565  fcdmnn0suppg  9567  cnref1o  10001  fztp  10434  fseq1m1p1  10451  fz0to4untppr  10480  frecuzrdgrrn  10794  frecuzrdgsuc  10800  frecuzrdgsuctlem  10809  seq3val  10846  seqvalcd  10847  fser0const  10921  mulexpzap  10965  expaddzap  10969  bcp1m1  11152  hashfibclem  11231  hash2en  11240  iswrdiz  11256  pfxccatin12lem2c  11447  cjexp  11603  rexuz3  11700  bdtri  11950  climconst  12000  sumfct  12084  zsumdc  12095  fsum3  12098  sum0  12099  fsumcnv  12148  mertenslem2  12247  zproddc  12290  fprodseq  12294  prod0  12296  prod1dc  12297  prodfct  12298  fprodcnv  12336  ef0lem  12371  efzval  12394  efival  12443  sinbnd  12463  cosbnd  12464  eucalgval  12776  eucalginv  12778  eucalglt  12779  eucalgcvga  12780  eucalg  12781  sqpweven  12897  2sqpwodd  12898  dfphi2  12942  phimullem  12947  prmdiv  12957  odzval  12964  pcval  13019  pczpre  13020  pcrec  13031  4sqlem17  13130  ballotfilemimin  13193  ennnfonelemhdmp1  13244  ennnfonelemkh  13247  ressinbasd  13371  restid2  13545  topnvalg  13548  imasival  13570  imasplusg  13572  qusval  13587  ismgm  13620  plusffvalg  13625  grpidvalg  13636  igsumvalx  13652  issgrp  13666  ismnddef  13679  ismhm  13716  isgrp  13761  grpn0  13790  grpinvfvalg  13797  grpsubfvalg  13800  mulgfvalg  13874  mulgval  13875  mulgnn0p1  13886  issubg  13926  isnsg  13955  eqgfval  13975  quseccl0g  13984  isghm  13996  conjsubg  14030  conjsubgen  14031  iscmn  14046  gfsumcl  14110  prdsval  14115  prdsbas3  14129  xpsval  14143  pwsval  14146  pwsbas  14147  pwselbasb  14148  pwsplusgval  14150  pwsmulrval  14151  pws0g  14155  pwsinvg  14157  mgpvalg  14162  isrng  14173  issrg  14208  isring  14243  iscrng  14246  opprvalg  14312  dfrhm2  14399  isnzr  14426  islring  14437  issubrg  14467  rrgval  14508  isdomn  14516  isdrngtap  14544  islmod  14565  scaffvalg  14580  lsssetm  14630  lspfval  14662  2idlval  14776  2idlvalg  14777  mulgrhm2  14884  zlmval  14901  znval  14910  znzrhfo  14922  znle2  14926  psrval  14940  mplvalcoe  14971  istps  15023  cldval  15090  ntrfval  15091  clsfval  15092  neifval  15131  restbasg  15159  tgrest  15160  txval  15246  upxp  15263  uptx  15265  txrest  15267  lmcn2  15271  cnmpt2t  15284  cnmpt2res  15288  imasnopn  15290  psmetxrge0  15323  xmetge0  15356  isxms  15442  isms  15444  bdxmet  15492  qtopbasss  15512  cnblcld  15526  mpomulcn  15557  negfcncf  15597  dvfvalap  15672  eldvap  15673  dvidlemap  15682  dvidrelem  15683  dvidsslem  15684  dvexp2  15703  dvrecap  15704  dveflem  15717  plyconst  15736  plycolemc  15749  sin0pilem1  15772  ptolemy  15815  coskpi  15839  logbrec  15951  mpodvdsmulf1o  15984  fsumdvdsmul  15985  lgslem1  15999  lgsval  16003  lgsval4  16019  lgsfcl3  16020  lgsdilem  16026  lgsdir2lem4  16030  lgsdir2lem5  16031  gausslemma2dlem5  16065  lgsquadlem2  16077  iedgedgg  16182  isuhgrm  16192  isushgrm  16193  isupgren  16216  isumgren  16226  isuspgren  16278  isusgren  16279  usgrstrrepeen  16352  vtxdgfval  16409  wksfval  16443  ifpsnprss  16464  clwwlkg  16514  clwwlkn1  16539  eupthsg  16566  eupth2fi  16600  nninfsellemqall  16919  qdiff  16959