Theorem eqtr4id 2258

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 2210	. 2 ⊢ 𝐵 = 𝐴
4	1, 3	eqtr2di 2256	1 ⊢ (𝜑 → 𝐴 = 𝐶)

Syntax hints:   → wi 4   = wceq 1373

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-cleq 2199

This theorem is referenced by:  iftrue  3577  iffalse  3580  difprsn1  3774  dmmptg  5185  relcoi1  5219  funimacnv  5355  dmmptd  5412  dffv3g  5579  dfimafn  5634  fvco2  5655  isoini  5894  iotaexel  5911  fvmpopr2d  6089  oprabco  6310  ixpconstg  6801  unfiexmid  7022  undifdc  7028  sbthlemi4  7069  sbthlemi5  7070  sbthlemi6  7071  supval2ti  7104  exmidfodomrlemim  7316  suplocexprlemex  7842  eqneg  8812  zeo  9485  fseq1p1m1  10223  seq3val  10612  seqvalcd  10613  hashfzo  10974  hashxp  10978  wrdval  11004  wrdnval  11031  fsumconst  11809  modfsummod  11813  telfsumo  11821  fprodconst  11975  mulgcd  12381  algcvg  12414  phiprmpw  12588  phisum  12607  strslfv3  12922  resseqnbasd  12949  pwssnf1o  13174  imasplusg  13184  imasmulr  13185  ismgmid  13253  pws0g  13327  dfrhm2  13960  subrg1  14037  2idlbas  14321  psrbagfi  14479  psrlinv  14490  mplbascoe  14497  mplplusgg  14509  uptx  14790  resubmet  15072  ply1termlem  15258  lgsval4lem  15532  lgsquadlem2  15599  m1lgs  15606