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 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 2213

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

This theorem is referenced by:  3eqtr4g  2289  rabxmdc  3528  ifpprsnssdc  3783  relop  4886  csbcnvg  4920  dfiun3g  4995  dfiin3g  4996  resima2  5053  relcnvfld  5277  uniabio  5304  fntpg  5393  dffn5im  5700  dfimafn2  5704  fncnvima2  5777  fmptcof  5822  fcoconst  5826  fnasrng  5836  funopsn  5838  fncofn  5840  ffnov  6135  fnovim  6140  fnrnov  6178  foov  6179  funimassov  6182  ovelimab  6183  ofc12  6268  caofinvl  6270  dftpos3  6471  tfr0dm  6531  rdgisucinc  6594  oasuc  6675  ecinxp  6822  phplem1  7081  exmidpw  7143  exmidpweq  7144  unfiin  7161  fidcenumlemr  7197  0ct  7349  ctmlemr  7350  exmidaclem  7466  pw1m  7485  indpi  7605  nqnq0pi  7701  nq0m0r  7719  addnqpr1  7825  recexgt0sr  8036  suplocsrlempr  8070  recidpipr  8119  recidpirq  8121  axrnegex  8142  nntopi  8157  fcdmnn0supp  9496  fcdmnn0suppg  9497  cnref1o  9929  fztp  10358  fseq1m1p1  10375  fz0to4untppr  10404  frecuzrdgrrn  10716  frecuzrdgsuc  10722  frecuzrdgsuctlem  10731  seq3val  10768  seqvalcd  10769  fser0const  10843  mulexpzap  10887  expaddzap  10891  bcp1m1  11073  hash2en  11153  iswrdiz  11169  pfxccatin12lem2c  11360  cjexp  11516  rexuz3  11613  bdtri  11863  climconst  11913  sumfct  11997  zsumdc  12008  fsum3  12011  sum0  12012  fsumcnv  12061  mertenslem2  12160  zproddc  12203  fprodseq  12207  prod0  12209  prod1dc  12210  prodfct  12211  fprodcnv  12249  ef0lem  12284  efzval  12307  efival  12356  sinbnd  12376  cosbnd  12377  eucalgval  12689  eucalginv  12691  eucalglt  12692  eucalgcvga  12693  eucalg  12694  sqpweven  12810  2sqpwodd  12811  dfphi2  12855  phimullem  12860  prmdiv  12870  odzval  12877  pcval  12932  pczpre  12933  pcrec  12944  4sqlem17  13043  ennnfonelemhdmp1  13093  ennnfonelemkh  13096  ressinbasd  13220  restid2  13394  topnvalg  13397  prdsval  13419  prdsbas3  13433  pwsval  13437  pwsbas  13438  pwselbasb  13439  pwsplusgval  13441  pwsmulrval  13442  imasival  13452  imasplusg  13454  qusval  13469  xpsval  13498  ismgm  13503  plusffvalg  13508  grpidvalg  13519  igsumvalx  13535  issgrp  13549  ismnddef  13564  pws0g  13597  ismhm  13607  isgrp  13652  grpn0  13681  grpinvfvalg  13688  grpsubfvalg  13691  pwsinvg  13758  mulgfvalg  13771  mulgval  13772  mulgnn0p1  13783  issubg  13823  isnsg  13852  eqgfval  13872  quseccl0g  13881  isghm  13893  conjsubg  13927  conjsubgen  13928  iscmn  13943  mgpvalg  14000  isrng  14011  issrg  14042  isring  14077  iscrng  14080  opprvalg  14146  dfrhm2  14232  isnzr  14259  islring  14270  issubrg  14299  rrgval  14340  isdomn  14348  islmod  14370  scaffvalg  14385  lsssetm  14435  lspfval  14467  2idlval  14581  2idlvalg  14582  mulgrhm2  14689  zlmval  14706  znval  14715  znzrhfo  14727  znle2  14731  psrval  14745  mplvalcoe  14774  istps  14826  cldval  14893  ntrfval  14894  clsfval  14895  neifval  14934  restbasg  14962  tgrest  14963  txval  15049  upxp  15066  uptx  15068  txrest  15070  lmcn2  15074  cnmpt2t  15087  cnmpt2res  15091  imasnopn  15093  psmetxrge0  15126  xmetge0  15159  isxms  15245  isms  15247  bdxmet  15295  qtopbasss  15315  cnblcld  15329  mpomulcn  15360  negfcncf  15400  dvfvalap  15475  eldvap  15476  dvidlemap  15485  dvidrelem  15486  dvidsslem  15487  dvexp2  15506  dvrecap  15507  dveflem  15520  plyconst  15539  plycolemc  15552  sin0pilem1  15575  ptolemy  15618  coskpi  15642  logbrec  15754  mpodvdsmulf1o  15787  fsumdvdsmul  15788  lgslem1  15802  lgsval  15806  lgsval4  15822  lgsfcl3  15823  lgsdilem  15829  lgsdir2lem4  15833  lgsdir2lem5  15834  gausslemma2dlem5  15868  lgsquadlem2  15880  iedgedgg  15985  isuhgrm  15995  isushgrm  15996  isupgren  16019  isumgren  16029  isuspgren  16081  isusgren  16082  usgrstrrepeen  16155  vtxdgfval  16212  wksfval  16246  ifpsnprss  16267  clwwlkg  16317  clwwlkn1  16342  eupthsg  16369  eupth2fi  16403  nninfsellemqall  16724  qdiff  16764  gfsumcl  16799