Theorem eqtr4di 2257

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

Syntax hints:   → wi 4   = wceq 1373

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2188

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

This theorem is referenced by:  3eqtr4g  2264  rabxmdc  3496  relop  4836  csbcnvg  4870  dfiun3g  4944  dfiin3g  4945  resima2  5002  relcnvfld  5225  uniabio  5251  fntpg  5339  dffn5im  5637  dfimafn2  5641  fncnvima2  5714  fmptcof  5760  fcoconst  5764  fnasrng  5773  funopsn  5775  ffnov  6062  fnovim  6067  fnrnov  6105  foov  6106  funimassov  6109  ovelimab  6110  ofc12  6195  caofinvl  6197  dftpos3  6361  tfr0dm  6421  rdgisucinc  6484  oasuc  6563  ecinxp  6710  phplem1  6964  exmidpw  7020  exmidpweq  7021  unfiin  7038  fidcenumlemr  7072  0ct  7224  ctmlemr  7225  exmidaclem  7336  pw1m  7355  indpi  7475  nqnq0pi  7571  nq0m0r  7589  addnqpr1  7695  recexgt0sr  7906  suplocsrlempr  7940  recidpipr  7989  recidpirq  7991  axrnegex  8012  nntopi  8027  cnref1o  9792  fztp  10220  fseq1m1p1  10237  fz0to4untppr  10266  frecuzrdgrrn  10575  frecuzrdgsuc  10581  frecuzrdgsuctlem  10590  seq3val  10627  seqvalcd  10628  fser0const  10702  mulexpzap  10746  expaddzap  10750  bcp1m1  10932  hash2en  11010  iswrdiz  11023  cjexp  11279  rexuz3  11376  bdtri  11626  climconst  11676  sumfct  11760  zsumdc  11770  fsum3  11773  sum0  11774  fsumcnv  11823  mertenslem2  11922  zproddc  11965  fprodseq  11969  prod0  11971  prod1dc  11972  prodfct  11973  fprodcnv  12011  ef0lem  12046  efzval  12069  efival  12118  sinbnd  12138  cosbnd  12139  eucalgval  12451  eucalginv  12453  eucalglt  12454  eucalgcvga  12455  eucalg  12456  sqpweven  12572  2sqpwodd  12573  dfphi2  12617  phimullem  12622  prmdiv  12632  odzval  12639  pcval  12694  pczpre  12695  pcrec  12706  4sqlem17  12805  ennnfonelemhdmp1  12855  ennnfonelemkh  12858  ressinbasd  12981  restid2  13155  topnvalg  13158  prdsval  13180  prdsbas3  13194  pwsval  13198  pwsbas  13199  pwselbasb  13200  pwsplusgval  13202  pwsmulrval  13203  imasival  13213  imasplusg  13215  qusval  13230  xpsval  13259  ismgm  13264  plusffvalg  13269  grpidvalg  13280  igsumvalx  13296  issgrp  13310  ismnddef  13325  pws0g  13358  ismhm  13368  isgrp  13413  grpn0  13442  grpinvfvalg  13449  grpsubfvalg  13452  pwsinvg  13519  mulgfvalg  13532  mulgval  13533  mulgnn0p1  13544  issubg  13584  isnsg  13613  eqgfval  13633  quseccl0g  13642  isghm  13654  conjsubg  13688  conjsubgen  13689  iscmn  13704  mgpvalg  13760  isrng  13771  issrg  13802  isring  13837  iscrng  13840  opprvalg  13906  dfrhm2  13991  isnzr  14018  islring  14029  issubrg  14058  rrgval  14099  isdomn  14106  islmod  14128  scaffvalg  14143  lsssetm  14193  lspfval  14225  2idlval  14339  2idlvalg  14340  mulgrhm2  14447  zlmval  14464  znval  14473  znzrhfo  14485  znle2  14489  psrval  14503  mplvalcoe  14527  istps  14579  cldval  14646  ntrfval  14647  clsfval  14648  neifval  14687  restbasg  14715  tgrest  14716  txval  14802  upxp  14819  uptx  14821  txrest  14823  lmcn2  14827  cnmpt2t  14840  cnmpt2res  14844  imasnopn  14846  psmetxrge0  14879  xmetge0  14912  isxms  14998  isms  15000  bdxmet  15048  qtopbasss  15068  cnblcld  15082  mpomulcn  15113  negfcncf  15153  dvfvalap  15228  eldvap  15229  dvidlemap  15238  dvidrelem  15239  dvidsslem  15240  dvexp2  15259  dvrecap  15260  dveflem  15273  plyconst  15292  plycolemc  15305  sin0pilem1  15328  ptolemy  15371  coskpi  15395  logbrec  15507  mpodvdsmulf1o  15537  fsumdvdsmul  15538  lgslem1  15552  lgsval  15556  lgsval4  15572  lgsfcl3  15573  lgsdilem  15579  lgsdir2lem4  15583  lgsdir2lem5  15584  gausslemma2dlem5  15618  lgsquadlem2  15630  iedgedgg  15732  isuhgrm  15742  isushgrm  15743  isupgren  15766  isumgren  15776  nninfsellemqall  16093