Theorem eqtr4id 2248

Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)

Hypotheses

Ref	Expression
eqtr4id.2	⊢ 𝐴 = 𝐵
eqtr4id.1	⊢ (𝜑 → 𝐶 = 𝐵)

Assertion

Ref	Expression
eqtr4id	⊢ (𝜑 → 𝐴 = 𝐶)

Proof of Theorem eqtr4id

Step	Hyp	Ref	Expression
1		eqtr4id.1	. 2 ⊢ (𝜑 → 𝐶 = 𝐵)
2		eqtr4id.2	. . 3 ⊢ 𝐴 = 𝐵
3	2	eqcomi 2200	. 2 ⊢ 𝐵 = 𝐴
4	1, 3	eqtr2di 2246	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:  iftrue  3567  iffalse  3570  difprsn1  3762  dmmptg  5168  relcoi1  5202  funimacnv  5335  dmmptd  5391  dffv3g  5557  dfimafn  5612  fvco2  5633  isoini  5868  iotaexel  5885  fvmpopr2d  6063  oprabco  6284  ixpconstg  6775  unfiexmid  6988  undifdc  6994  sbthlemi4  7035  sbthlemi5  7036  sbthlemi6  7037  supval2ti  7070  exmidfodomrlemim  7282  suplocexprlemex  7808  eqneg  8778  zeo  9450  fseq1p1m1  10188  seq3val  10571  seqvalcd  10572  hashfzo  10933  hashxp  10937  wrdval  10957  wrdnval  10984  fsumconst  11638  modfsummod  11642  telfsumo  11650  fprodconst  11804  mulgcd  12210  algcvg  12243  phiprmpw  12417  phisum  12436  strslfv3  12751  resseqnbasd  12778  pwssnf1o  13002  imasplusg  13012  imasmulr  13013  ismgmid  13081  pws0g  13155  dfrhm2  13788  subrg1  13865  2idlbas  14149  psrlinv  14314  uptx  14596  resubmet  14878  ply1termlem  15064  lgsval4lem  15338  lgsquadlem2  15405  m1lgs  15412