Theorem eqtr4di 2285

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 2238	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	eqtrdi 2283	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 2216

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

This theorem is referenced by:  3eqtr4g  2292  rabxmdc  3544  ifpprsnssdc  3805  relop  4911  csbcnvg  4945  dfiun3g  5020  dfiin3g  5021  resima2  5078  relcnvfld  5302  uniabio  5329  fntpg  5418  dffn5im  5728  dfimafn2  5732  fncnvima2  5805  fmptcof  5850  fcoconst  5854  fnasrng  5864  funopsn  5866  fncofn  5868  ffnov  6166  fnovim  6171  fnrnov  6209  foov  6210  funimassov  6213  ovelimab  6214  ofc12  6300  caofinvl  6302  dftpos3  6507  tfr0dm  6567  rdgisucinc  6630  oasuc  6711  ecinxp  6858  mapunen  7118  phplem1  7120  exmidpw  7182  exmidpweq  7183  unfiin  7200  fidcenumlemr  7239  0ct  7412  ctmlemr  7413  exmidaclem  7529  pw1m  7548  indpi  7674  nqnq0pi  7770  nq0m0r  7788  addnqpr1  7894  recexgt0sr  8105  suplocsrlempr  8139  recidpipr  8188  recidpirq  8190  axrnegex  8211  nntopi  8226  fcdmnn0supp  9569  fcdmnn0suppg  9571  cnref1o  10005  fztp  10438  fseq1m1p1  10455  fz0to4untppr  10484  frecuzrdgrrn  10798  frecuzrdgsuc  10804  frecuzrdgsuctlem  10813  seq3val  10850  seqvalcd  10851  fser0const  10925  mulexpzap  10969  expaddzap  10973  bcp1m1  11156  hashfibclem  11235  hash2en  11244  iswrdiz  11260  pfxccatin12lem2c  11451  cjexp  11607  rexuz3  11705  bdtri  11955  climconst  12005  sumfct  12089  zsumdc  12100  fsum3  12103  sum0  12104  fsumcnv  12153  mertenslem2  12252  zproddc  12295  fprodseq  12299  prod0  12301  prod1dc  12302  prodfct  12303  fprodcnv  12341  ef0lem  12376  efzval  12399  efival  12448  sinbnd  12468  cosbnd  12469  eucalgval  12781  eucalginv  12783  eucalglt  12784  eucalgcvga  12785  eucalg  12786  sqpweven  12902  2sqpwodd  12903  dfphi2  12947  phimullem  12952  prmdiv  12962  odzval  12969  pcval  13024  pczpre  13025  pcrec  13036  4sqlem17  13135  ballotfilemimin  13198  ennnfonelemhdmp1  13249  ennnfonelemkh  13252  ressinbasd  13376  restid2  13550  topnvalg  13553  imasival  13575  imasplusg  13577  qusval  13592  ismgm  13625  plusffvalg  13630  grpidvalg  13641  igsumvalx  13657  issgrp  13671  ismnddef  13684  ismhm  13721  isgrp  13766  grpn0  13795  grpinvfvalg  13802  grpsubfvalg  13805  mulgfvalg  13879  mulgval  13880  mulgnn0p1  13891  issubg  13931  isnsg  13960  eqgfval  13980  quseccl0g  13989  isghm  14001  conjsubg  14035  conjsubgen  14036  iscmn  14051  gfsumcl  14115  prdsval  14120  prdsbas3  14134  xpsval  14148  pwsval  14151  pwsbas  14152  pwselbasb  14153  pwsplusgval  14155  pwsmulrval  14156  pws0g  14160  pwsinvg  14162  mgpvalg  14167  isrng  14178  issrg  14213  isring  14248  iscrng  14251  opprvalg  14317  dfrhm2  14404  isnzr  14431  islring  14442  issubrg  14472  rrgval  14513  isdomn  14521  isdrngtap  14549  islmod  14570  scaffvalg  14585  lsssetm  14635  lspfval  14667  2idlval  14781  2idlvalg  14782  mulgrhm2  14889  zlmval  14906  znval  14915  znzrhfo  14927  znle2  14931  psrval  14945  mplvalcoe  14976  istps  15028  cldval  15095  ntrfval  15096  clsfval  15097  neifval  15136  restbasg  15164  tgrest  15165  txval  15251  upxp  15268  uptx  15270  txrest  15272  lmcn2  15276  cnmpt2t  15289  cnmpt2res  15293  imasnopn  15295  psmetxrge0  15328  xmetge0  15361  isxms  15447  isms  15449  bdxmet  15497  qtopbasss  15517  cnblcld  15531  mpomulcn  15562  negfcncf  15602  dvfvalap  15677  eldvap  15678  dvidlemap  15687  dvidrelem  15688  dvidsslem  15689  dvexp2  15708  dvrecap  15709  dveflem  15722  plyconst  15741  plycolemc  15754  sin0pilem1  15777  ptolemy  15820  coskpi  15844  logbrec  15956  mpodvdsmulf1o  15989  fsumdvdsmul  15990  lgslem1  16004  lgsval  16008  lgsval4  16024  lgsfcl3  16025  lgsdilem  16031  lgsdir2lem4  16035  lgsdir2lem5  16036  gausslemma2dlem5  16070  lgsquadlem2  16082  iedgedgg  16187  isuhgrm  16197  isushgrm  16198  isupgren  16221  isumgren  16231  isuspgren  16283  isusgren  16284  usgrstrrepeen  16357  vtxdgfval  16414  wksfval  16448  ifpsnprss  16469  clwwlkg  16519  clwwlkn1  16544  eupthsg  16571  eupth2fi  16605  nninfsellemqall  16934  qdiff  16974