Theorem eqtr4id 2222

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

Syntax hints:   → wi 4   = wceq 1348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163

This theorem is referenced by:  iftrue  3531  iffalse  3534  difprsn1  3719  dmmptg  5108  relcoi1  5142  funimacnv  5274  dmmptd  5328  dffv3g  5492  dfimafn  5545  fvco2  5565  isoini  5797  oprabco  6196  ixpconstg  6685  unfiexmid  6895  undifdc  6901  sbthlemi4  6937  sbthlemi5  6938  sbthlemi6  6939  supval2ti  6972  exmidfodomrlemim  7178  suplocexprlemex  7684  eqneg  8649  zeo  9317  fseq1p1m1  10050  seq3val  10414  seqvalcd  10415  hashfzo  10757  hashxp  10761  fsumconst  11417  modfsummod  11421  telfsumo  11429  fprodconst  11583  mulgcd  11971  algcvg  12002  phiprmpw  12176  phisum  12194  strslfv3  12461  ismgmid  12631  uptx  13068  resubmet  13342  lgsval4lem  13706