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  7280  suplocexprlemex  7806  eqneg  8776  zeo  9448  fseq1p1m1  10186  seq3val  10569  seqvalcd  10570  hashfzo  10931  hashxp  10935  wrdval  10955  wrdnval  10982  fsumconst  11636  modfsummod  11640  telfsumo  11648  fprodconst  11802  mulgcd  12208  algcvg  12241  phiprmpw  12415  phisum  12434  strslfv3  12749  resseqnbasd  12776  pwssnf1o  13000  imasplusg  13010  imasmulr  13011  ismgmid  13079  pws0g  13153  dfrhm2  13786  subrg1  13863  2idlbas  14147  psrlinv  14312  uptx  14594  resubmet  14876  ply1termlem  15062  lgsval4lem  15336  lgsquadlem2  15403  m1lgs  15410