Theorem eqtr4id 2286

Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)

Hypotheses

Ref	Expression
eqtr4id.2	|- A = B
eqtr4id.1	|- ( ph -> C = B )

Assertion

Ref	Expression
eqtr4id	|- ( ph -> A = C )

Proof of Theorem eqtr4id

Step	Hyp	Ref	Expression
1		eqtr4id.1	. 2 |- ( ph -> C = B )
2		eqtr4id.2	. . 3 |- A = B
3	2	eqcomi 2238	. 2 |- B = A
4	1, 3	eqtr2di 2284	1 |- ( ph -> A = C )

Syntax hints:   -> wi 4   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2216

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

This theorem is referenced by:  iftrue  3631  iffalse  3634  difprsn1  3838  dmmptg  5265  relcoi1  5299  funimacnv  5437  dmmptd  5494  dffv3g  5671  dfimafn  5730  fvco2  5751  dfimafnf  5928  isoini  5997  iotaexel  6016  fvmpopr2d  6198  oprabco  6426  suppcofn  6479  ixpconstg  6955  unfiexmid  7191  undifdc  7197  sbthlemi4  7243  sbthlemi5  7244  sbthlemi6  7245  supval2ti  7299  exmidfodomrlemim  7517  suplocexprlemex  8053  eqneg  9023  zeo  9701  fseq1p1m1  10450  seq3val  10846  seqvalcd  10847  hashfzo  11212  hashxp  11216  hashfibclem  11231  wrdval  11252  wrdnval  11280  swrdccat3blem  11456  fsumconst  12165  modfsummod  12169  telfsumo  12177  fprodconst  12331  mulgcd  12737  algcvg  12770  phiprmpw  12944  phisum  12963  strslfv3  13342  resseqnbasd  13370  imasplusg  13572  imasmulr  13573  ismgmid  13640  gsumshift  14105  pwssnf1o  14153  pws0g  14155  dfrhm2  14399  subrg1  14477  2idlbas  14789  psrbagfi  14949  psrlinv  14965  mplbascoe  14972  mplplusgg  14984  uptx  15265  resubmet  15547  ply1termlem  15733  lgsval4lem  16010  lgsquadlem2  16077  m1lgs  16084  uspgrf1oedg  16297