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  3524  ifpprsnssdc  3777  relop  4878  csbcnvg  4912  dfiun3g  4987  dfiin3g  4988  resima2  5045  relcnvfld  5268  uniabio  5295  fntpg  5383  dffn5im  5687  dfimafn2  5691  fncnvima2  5764  fmptcof  5810  fcoconst  5814  fnasrng  5823  funopsn  5825  fncofn  5827  ffnov  6120  fnovim  6125  fnrnov  6163  foov  6164  funimassov  6167  ovelimab  6168  ofc12  6254  caofinvl  6256  dftpos3  6423  tfr0dm  6483  rdgisucinc  6546  oasuc  6627  ecinxp  6774  phplem1  7033  exmidpw  7093  exmidpweq  7094  unfiin  7111  fidcenumlemr  7145  0ct  7297  ctmlemr  7298  exmidaclem  7413  pw1m  7432  indpi  7552  nqnq0pi  7648  nq0m0r  7666  addnqpr1  7772  recexgt0sr  7983  suplocsrlempr  8017  recidpipr  8066  recidpirq  8068  axrnegex  8089  nntopi  8104  cnref1o  9875  fztp  10303  fseq1m1p1  10320  fz0to4untppr  10349  frecuzrdgrrn  10660  frecuzrdgsuc  10666  frecuzrdgsuctlem  10675  seq3val  10712  seqvalcd  10713  fser0const  10787  mulexpzap  10831  expaddzap  10835  bcp1m1  11017  hash2en  11097  iswrdiz  11110  pfxccatin12lem2c  11301  cjexp  11444  rexuz3  11541  bdtri  11791  climconst  11841  sumfct  11925  zsumdc  11935  fsum3  11938  sum0  11939  fsumcnv  11988  mertenslem2  12087  zproddc  12130  fprodseq  12134  prod0  12136  prod1dc  12137  prodfct  12138  fprodcnv  12176  ef0lem  12211  efzval  12234  efival  12283  sinbnd  12303  cosbnd  12304  eucalgval  12616  eucalginv  12618  eucalglt  12619  eucalgcvga  12620  eucalg  12621  sqpweven  12737  2sqpwodd  12738  dfphi2  12782  phimullem  12787  prmdiv  12797  odzval  12804  pcval  12859  pczpre  12860  pcrec  12871  4sqlem17  12970  ennnfonelemhdmp1  13020  ennnfonelemkh  13023  ressinbasd  13147  restid2  13321  topnvalg  13324  prdsval  13346  prdsbas3  13360  pwsval  13364  pwsbas  13365  pwselbasb  13366  pwsplusgval  13368  pwsmulrval  13369  imasival  13379  imasplusg  13381  qusval  13396  xpsval  13425  ismgm  13430  plusffvalg  13435  grpidvalg  13446  igsumvalx  13462  issgrp  13476  ismnddef  13491  pws0g  13524  ismhm  13534  isgrp  13579  grpn0  13608  grpinvfvalg  13615  grpsubfvalg  13618  pwsinvg  13685  mulgfvalg  13698  mulgval  13699  mulgnn0p1  13710  issubg  13750  isnsg  13779  eqgfval  13799  quseccl0g  13808  isghm  13820  conjsubg  13854  conjsubgen  13855  iscmn  13870  mgpvalg  13926  isrng  13937  issrg  13968  isring  14003  iscrng  14006  opprvalg  14072  dfrhm2  14158  isnzr  14185  islring  14196  issubrg  14225  rrgval  14266  isdomn  14273  islmod  14295  scaffvalg  14310  lsssetm  14360  lspfval  14392  2idlval  14506  2idlvalg  14507  mulgrhm2  14614  zlmval  14631  znval  14640  znzrhfo  14652  znle2  14656  psrval  14670  mplvalcoe  14694  istps  14746  cldval  14813  ntrfval  14814  clsfval  14815  neifval  14854  restbasg  14882  tgrest  14883  txval  14969  upxp  14986  uptx  14988  txrest  14990  lmcn2  14994  cnmpt2t  15007  cnmpt2res  15011  imasnopn  15013  psmetxrge0  15046  xmetge0  15079  isxms  15165  isms  15167  bdxmet  15215  qtopbasss  15235  cnblcld  15249  mpomulcn  15280  negfcncf  15320  dvfvalap  15395  eldvap  15396  dvidlemap  15405  dvidrelem  15406  dvidsslem  15407  dvexp2  15426  dvrecap  15427  dveflem  15440  plyconst  15459  plycolemc  15472  sin0pilem1  15495  ptolemy  15538  coskpi  15562  logbrec  15674  mpodvdsmulf1o  15704  fsumdvdsmul  15705  lgslem1  15719  lgsval  15723  lgsval4  15739  lgsfcl3  15740  lgsdilem  15746  lgsdir2lem4  15750  lgsdir2lem5  15751  gausslemma2dlem5  15785  lgsquadlem2  15797  iedgedgg  15902  isuhgrm  15912  isushgrm  15913  isupgren  15936  isumgren  15946  isuspgren  15996  isusgren  15997  usgrstrrepeen  16070  vtxdgfval  16094  wksfval  16119  ifpsnprss  16140  clwwlkg  16188  clwwlkn1  16213  eupthsg  16240  nninfsellemqall  16553