Theorem eqtr4id 2282

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

Syntax hints:   → wi 4   = wceq 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2212

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

This theorem is referenced by:  iftrue  3611  iffalse  3614  difprsn1  3813  dmmptg  5236  relcoi1  5270  funimacnv  5408  dmmptd  5465  dffv3g  5638  dfimafn  5697  fvco2  5718  isoini  5964  iotaexel  5981  fvmpopr2d  6163  oprabco  6387  ixpconstg  6881  unfiexmid  7115  undifdc  7121  sbthlemi4  7164  sbthlemi5  7165  sbthlemi6  7166  supval2ti  7199  exmidfodomrlemim  7417  suplocexprlemex  7947  eqneg  8917  zeo  9590  fseq1p1m1  10334  seq3val  10728  seqvalcd  10729  hashfzo  11092  hashxp  11096  wrdval  11125  wrdnval  11153  swrdccat3blem  11329  fsumconst  12038  modfsummod  12042  telfsumo  12050  fprodconst  12204  mulgcd  12610  algcvg  12643  phiprmpw  12817  phisum  12836  strslfv3  13151  resseqnbasd  13179  pwssnf1o  13404  imasplusg  13414  imasmulr  13415  ismgmid  13483  pws0g  13557  dfrhm2  14192  subrg1  14269  2idlbas  14553  psrbagfi  14712  psrlinv  14727  mplbascoe  14734  mplplusgg  14746  uptx  15027  resubmet  15309  ply1termlem  15495  lgsval4lem  15769  lgsquadlem2  15836  m1lgs  15843  uspgrf1oedg  16056  gsumgfsumlem  16751