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  7091  undifdc  7097  sbthlemi4  7138  sbthlemi5  7139  sbthlemi6  7140  supval2ti  7173  exmidfodomrlemim  7390  suplocexprlemex  7920  eqneg  8890  zeo  9563  fseq1p1m1  10302  seq3val  10694  seqvalcd  10695  hashfzo  11057  hashxp  11061  wrdval  11087  wrdnval  11115  swrdccat3blem  11287  fsumconst  11981  modfsummod  11985  telfsumo  11993  fprodconst  12147  mulgcd  12553  algcvg  12586  phiprmpw  12760  phisum  12779  strslfv3  13094  resseqnbasd  13122  pwssnf1o  13347  imasplusg  13357  imasmulr  13358  ismgmid  13426  pws0g  13500  dfrhm2  14134  subrg1  14211  2idlbas  14495  psrbagfi  14653  psrlinv  14664  mplbascoe  14671  mplplusgg  14683  uptx  14964  resubmet  15246  ply1termlem  15432  lgsval4lem  15706  lgsquadlem2  15773  m1lgs  15780  uspgrf1oedg  15990