Theorem eqtr4di 2247

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

Syntax hints:   → wi 4   = wceq 1364

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  3eqtr4g  2254  rabxmdc  3482  relop  4816  csbcnvg  4850  dfiun3g  4923  dfiin3g  4924  resima2  4980  relcnvfld  5203  uniabio  5229  fntpg  5314  dffn5im  5606  dfimafn2  5610  fncnvima2  5683  fmptcof  5729  fcoconst  5733  fnasrng  5742  ffnov  6026  fnovim  6031  fnrnov  6069  foov  6070  funimassov  6073  ovelimab  6074  ofc12  6158  caofinvl  6160  dftpos3  6320  tfr0dm  6380  rdgisucinc  6443  oasuc  6522  ecinxp  6669  phplem1  6913  exmidpw  6969  exmidpweq  6970  unfiin  6987  fidcenumlemr  7021  0ct  7173  ctmlemr  7174  exmidaclem  7275  indpi  7409  nqnq0pi  7505  nq0m0r  7523  addnqpr1  7629  recexgt0sr  7840  suplocsrlempr  7874  recidpipr  7923  recidpirq  7925  axrnegex  7946  nntopi  7961  cnref1o  9725  fztp  10153  fseq1m1p1  10170  fz0to4untppr  10199  frecuzrdgrrn  10500  frecuzrdgsuc  10506  frecuzrdgsuctlem  10515  seq3val  10552  seqvalcd  10553  fser0const  10627  mulexpzap  10671  expaddzap  10675  bcp1m1  10857  iswrdiz  10942  cjexp  11058  rexuz3  11155  bdtri  11405  climconst  11455  sumfct  11539  zsumdc  11549  fsum3  11552  sum0  11553  fsumcnv  11602  mertenslem2  11701  zproddc  11744  fprodseq  11748  prod0  11750  prod1dc  11751  prodfct  11752  fprodcnv  11790  ef0lem  11825  efzval  11848  efival  11897  sinbnd  11917  cosbnd  11918  eucalgval  12222  eucalginv  12224  eucalglt  12225  eucalgcvga  12226  eucalg  12227  sqpweven  12343  2sqpwodd  12344  dfphi2  12388  phimullem  12393  prmdiv  12403  odzval  12410  pcval  12465  pczpre  12466  pcrec  12477  4sqlem17  12576  ennnfonelemhdmp1  12626  ennnfonelemkh  12629  ressinbasd  12752  restid2  12919  topnvalg  12922  imasival  12949  imasplusg  12951  qusval  12966  xpsval  12995  ismgm  13000  plusffvalg  13005  grpidvalg  13016  igsumvalx  13032  issgrp  13046  ismnddef  13059  ismhm  13093  isgrp  13138  grpn0  13167  grpinvfvalg  13174  grpsubfvalg  13177  mulgfvalg  13251  mulgval  13252  mulgnn0p1  13263  issubg  13303  isnsg  13332  eqgfval  13352  quseccl0g  13361  isghm  13373  conjsubg  13407  conjsubgen  13408  iscmn  13423  mgpvalg  13479  isrng  13490  issrg  13521  isring  13556  iscrng  13559  opprvalg  13625  dfrhm2  13710  isnzr  13737  islring  13748  issubrg  13777  rrgval  13818  isdomn  13825  islmod  13847  scaffvalg  13862  lsssetm  13912  lspfval  13944  2idlval  14058  2idlvalg  14059  mulgrhm2  14166  zlmval  14183  znval  14192  znzrhfo  14204  znle2  14208  psrval  14220  istps  14268  cldval  14335  ntrfval  14336  clsfval  14337  neifval  14376  restbasg  14404  tgrest  14405  txval  14491  upxp  14508  uptx  14510  txrest  14512  lmcn2  14516  cnmpt2t  14529  cnmpt2res  14533  imasnopn  14535  psmetxrge0  14568  xmetge0  14601  isxms  14687  isms  14689  bdxmet  14737  qtopbasss  14757  cnblcld  14771  mpomulcn  14802  negfcncf  14842  dvfvalap  14917  eldvap  14918  dvidlemap  14927  dvidrelem  14928  dvidsslem  14929  dvexp2  14948  dvrecap  14949  dveflem  14962  plyconst  14981  plycolemc  14994  sin0pilem1  15017  ptolemy  15060  coskpi  15084  logbrec  15196  mpodvdsmulf1o  15226  fsumdvdsmul  15227  lgslem1  15241  lgsval  15245  lgsval4  15261  lgsfcl3  15262  lgsdilem  15268  lgsdir2lem4  15272  lgsdir2lem5  15273  gausslemma2dlem5  15307  lgsquadlem2  15319  nninfsellemqall  15659