Theorem eqtr4id 2281

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 2233	. 2 ⊢ 𝐵 = 𝐴
4	1, 3	eqtr2di 2279	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:  iftrue  3607  iffalse  3610  difprsn1  3807  dmmptg  5226  relcoi1  5260  funimacnv  5397  dmmptd  5454  dffv3g  5625  dfimafn  5684  fvco2  5705  isoini  5948  iotaexel  5965  fvmpopr2d  6147  oprabco  6369  ixpconstg  6862  unfiexmid  7088  undifdc  7094  sbthlemi4  7135  sbthlemi5  7136  sbthlemi6  7137  supval2ti  7170  exmidfodomrlemim  7387  suplocexprlemex  7917  eqneg  8887  zeo  9560  fseq1p1m1  10298  seq3val  10690  seqvalcd  10691  hashfzo  11052  hashxp  11056  wrdval  11082  wrdnval  11110  swrdccat3blem  11279  fsumconst  11973  modfsummod  11977  telfsumo  11985  fprodconst  12139  mulgcd  12545  algcvg  12578  phiprmpw  12752  phisum  12771  strslfv3  13086  resseqnbasd  13114  pwssnf1o  13339  imasplusg  13349  imasmulr  13350  ismgmid  13418  pws0g  13492  dfrhm2  14126  subrg1  14203  2idlbas  14487  psrbagfi  14645  psrlinv  14656  mplbascoe  14663  mplplusgg  14675  uptx  14956  resubmet  15238  ply1termlem  15424  lgsval4lem  15698  lgsquadlem2  15765  m1lgs  15772  uspgrf1oedg  15982