Theorem eqtr4di 2280

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

Syntax hints:   → wi 4   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  3eqtr4g  2287  rabxmdc  3523  relop  4871  csbcnvg  4905  dfiun3g  4980  dfiin3g  4981  resima2  5038  relcnvfld  5261  uniabio  5288  fntpg  5376  dffn5im  5678  dfimafn2  5682  fncnvima2  5755  fmptcof  5801  fcoconst  5805  fnasrng  5814  funopsn  5816  ffnov  6107  fnovim  6112  fnrnov  6150  foov  6151  funimassov  6154  ovelimab  6155  ofc12  6240  caofinvl  6242  dftpos3  6406  tfr0dm  6466  rdgisucinc  6529  oasuc  6608  ecinxp  6755  phplem1  7009  exmidpw  7066  exmidpweq  7067  unfiin  7084  fidcenumlemr  7118  0ct  7270  ctmlemr  7271  exmidaclem  7386  pw1m  7405  indpi  7525  nqnq0pi  7621  nq0m0r  7639  addnqpr1  7745  recexgt0sr  7956  suplocsrlempr  7990  recidpipr  8039  recidpirq  8041  axrnegex  8062  nntopi  8077  cnref1o  9842  fztp  10270  fseq1m1p1  10287  fz0to4untppr  10316  frecuzrdgrrn  10625  frecuzrdgsuc  10631  frecuzrdgsuctlem  10640  seq3val  10677  seqvalcd  10678  fser0const  10752  mulexpzap  10796  expaddzap  10800  bcp1m1  10982  hash2en  11060  iswrdiz  11073  pfxccatin12lem2c  11257  cjexp  11399  rexuz3  11496  bdtri  11746  climconst  11796  sumfct  11880  zsumdc  11890  fsum3  11893  sum0  11894  fsumcnv  11943  mertenslem2  12042  zproddc  12085  fprodseq  12089  prod0  12091  prod1dc  12092  prodfct  12093  fprodcnv  12131  ef0lem  12166  efzval  12189  efival  12238  sinbnd  12258  cosbnd  12259  eucalgval  12571  eucalginv  12573  eucalglt  12574  eucalgcvga  12575  eucalg  12576  sqpweven  12692  2sqpwodd  12693  dfphi2  12737  phimullem  12742  prmdiv  12752  odzval  12759  pcval  12814  pczpre  12815  pcrec  12826  4sqlem17  12925  ennnfonelemhdmp1  12975  ennnfonelemkh  12978  ressinbasd  13102  restid2  13276  topnvalg  13279  prdsval  13301  prdsbas3  13315  pwsval  13319  pwsbas  13320  pwselbasb  13321  pwsplusgval  13323  pwsmulrval  13324  imasival  13334  imasplusg  13336  qusval  13351  xpsval  13380  ismgm  13385  plusffvalg  13390  grpidvalg  13401  igsumvalx  13417  issgrp  13431  ismnddef  13446  pws0g  13479  ismhm  13489  isgrp  13534  grpn0  13563  grpinvfvalg  13570  grpsubfvalg  13573  pwsinvg  13640  mulgfvalg  13653  mulgval  13654  mulgnn0p1  13665  issubg  13705  isnsg  13734  eqgfval  13754  quseccl0g  13763  isghm  13775  conjsubg  13809  conjsubgen  13810  iscmn  13825  mgpvalg  13881  isrng  13892  issrg  13923  isring  13958  iscrng  13961  opprvalg  14027  dfrhm2  14112  isnzr  14139  islring  14150  issubrg  14179  rrgval  14220  isdomn  14227  islmod  14249  scaffvalg  14264  lsssetm  14314  lspfval  14346  2idlval  14460  2idlvalg  14461  mulgrhm2  14568  zlmval  14585  znval  14594  znzrhfo  14606  znle2  14610  psrval  14624  mplvalcoe  14648  istps  14700  cldval  14767  ntrfval  14768  clsfval  14769  neifval  14808  restbasg  14836  tgrest  14837  txval  14923  upxp  14940  uptx  14942  txrest  14944  lmcn2  14948  cnmpt2t  14961  cnmpt2res  14965  imasnopn  14967  psmetxrge0  15000  xmetge0  15033  isxms  15119  isms  15121  bdxmet  15169  qtopbasss  15189  cnblcld  15203  mpomulcn  15234  negfcncf  15274  dvfvalap  15349  eldvap  15350  dvidlemap  15359  dvidrelem  15360  dvidsslem  15361  dvexp2  15380  dvrecap  15381  dveflem  15394  plyconst  15413  plycolemc  15426  sin0pilem1  15449  ptolemy  15492  coskpi  15516  logbrec  15628  mpodvdsmulf1o  15658  fsumdvdsmul  15659  lgslem1  15673  lgsval  15677  lgsval4  15693  lgsfcl3  15694  lgsdilem  15700  lgsdir2lem4  15704  lgsdir2lem5  15705  gausslemma2dlem5  15739  lgsquadlem2  15751  iedgedgg  15855  isuhgrm  15865  isushgrm  15866  isupgren  15889  isumgren  15899  isuspgren  15949  isusgren  15950  usgrstrrepeen  16023  wksfval  16028  ifpsnprss  16040  nninfsellemqall  16340