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  5229  relcoi1  5263  funimacnv  5400  dmmptd  5457  dffv3g  5628  dfimafn  5687  fvco2  5708  isoini  5951  iotaexel  5968  fvmpopr2d  6150  oprabco  6374  ixpconstg  6867  unfiexmid  7096  undifdc  7102  sbthlemi4  7143  sbthlemi5  7144  sbthlemi6  7145  supval2ti  7178  exmidfodomrlemim  7395  suplocexprlemex  7925  eqneg  8895  zeo  9568  fseq1p1m1  10307  seq3val  10699  seqvalcd  10700  hashfzo  11062  hashxp  11066  wrdval  11092  wrdnval  11120  swrdccat3blem  11292  fsumconst  11986  modfsummod  11990  telfsumo  11998  fprodconst  12152  mulgcd  12558  algcvg  12591  phiprmpw  12765  phisum  12784  strslfv3  13099  resseqnbasd  13127  pwssnf1o  13352  imasplusg  13362  imasmulr  13363  ismgmid  13431  pws0g  13505  dfrhm2  14139  subrg1  14216  2idlbas  14500  psrbagfi  14658  psrlinv  14669  mplbascoe  14676  mplplusgg  14688  uptx  14969  resubmet  15251  ply1termlem  15437  lgsval4lem  15711  lgsquadlem2  15778  m1lgs  15785  uspgrf1oedg  15995