Theorem eqtr3d 1546

Description: An equality transitivity equality deduction.

Hypotheses

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

Assertion

Ref	Expression
eqtr3d	|- (ph -> B = C)

Proof of Theorem eqtr3d

Step	Hyp	Ref	Expression
1		eqtr3d.1	. . 3 |- (ph -> A = B)
2	1	eqcomd 1517	. 2 |- (ph -> B = A)
3		eqtr3d.2	. 2 |- (ph -> A = C)
4	2, 3	eqtrd 1544	1 |- (ph -> B = C)

Syntax hints:   -> wi 3   = wceq 988

This theorem is referenced by:  3eqtrrd 1549  3eqtr3d 1552  3eqtr3rd 1553  csbnestg 2080  uneqin 2300  f00 3732  f1imacnv 3781  f1ococnv1 3785  fvsnun2 3872  oprssoprval 4112  caoprmo 4148  oaabs 4336  map0b 4430  mapsn 4432  en1 4513  ssenen 4593  1qec 5157  halfpq 5171  pn0sr 5299  mulgt0sr 5303  cnegexlem2 5435  cnegex 5437  csbnegg 5453  subadd23 5474  addsub12 5475  subneg 5483  pncan2 5487  npcan 5488  npncan 5489  subdi 5516  subsub2 5550  subsub 5551  nnncan1 5556  nnncan2 5557  nppcan2 5559  mulsub 5566  recex 5773  divsubdir 5854  divsubdirOLD 5855  divmuldiv 5861  divmuldivOLD 5862  divdivdiv 5867  divdivdivOLD 5868  divcan6 5874  qreccl 6353  modid 6409  2shfti 6645  shftcan1 6647  seqzval2 6676  expm1t 6706  expadd 6719  expsubOLD 6721  expordi 6722  subsq 6764  subsq2 6765  imre 6896  imcj 6942  sqabsadd 6971  sqabssub 6972  absreim 6980  absdivzi 6982  absnid 6986  recvalzi 7010  abs1mi 7027  ser1absdiflem 7052  facndiv 7066  bcpasci 7092  serzfsum 7127  serz0 7176  binomlem5 7193  bcxmaslem2 7198  bcxmas 7199  iserzshft2i 7230  climrecl 7233  climge0 7235  climaddlem3 7239  climcji 7273  geoseri 7357  cjcncf 7401  mulc1cncf 7402  efcan 7491  efexp 7495  efnn0val 7496  resinval 7557  recosval 7558  cos2t 7587  cos2tsin 7588  sin01bndlem3 7594  cos01bndlem3 7596  iincld 7799  metcnss 8018  metcnss2 8019  grpidinvlem1 8168  grpidinvlem3 8170  grpinvid1 8191  grpinvid2 8192  isgrp2i 8195  grpnpncan 8213  resgrprn 8214  abldivdiv 8227  subgid 8239  cnaddabl 8245  ghgrpilem3 8254  vc2 8293  vcsubdir 8294  vcm 8309  vcnegneg 8312  nvpncan 8396  nvnpcan 8399  nvnncan 8402  nvdif 8412  nvpi 8413  nvge0 8421  imsmetlem 8442  ip0l 8490  ipasslem2 8610  ipasslem4 8612  ipasslem9 8617  ubthlem8 8655  minveclem19 8682  minveclem35 8698  minveclem36 8699  htthlem9 8747  sinperlem1 8804  sin2pim 8810  cos2pim 8811  sinkpi 8816  sincosq2sgn 8824  sincosq3sgn 8825  sincosq4sgn 8826  sinq12gt0t 8827  sincosq1eq 8828  abssinper 8831  sineq0 8832  shftefif1olem 8860  effoi 8864  eflog 8879  logef 8881  relogoprlem 8888  relogexp 8893  hvaddid2 9011  hvmul0 9012  hvnegid 9015  hvm1neg 9020  hvpncan2 9028  hvpncan3 9030  hvsubdistr2 9036  hhph 9165  chdmj1 9572  h1de2bi 9597  spansncol 9611  h1datomi 9624  fh1 9681  fh2 9682  5oalem1 9719  3oalem2 9728  pjvec 9761  pjocvec 9762  pjdsi 9777  mayete3i 9793  hosubneg 9853  hosubsub2 9858  hosubsub 9863  cnvunop 9960  unopadj 9961  kbmul 9997  nlelchi 10111  riesz3i 10112  riesz4i 10113  nmopcoadji 10151  branmfn 10155  cnvbramul 10165  leopnmid 10188  nmopleid 10189  hmopidmpji 10197  pjclem4 10245  pj3si 10253  hstoc 10267  hst1h 10272  hstle 10275  sto1i 10281  superpos 10399  cvexchlem 10413  atomli 10427  atordi 10429  irredlem3 10437  mdsymlem1 10448  dmdbr5ati 10467  cdj3lem3 10483  2wsms 10766

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 995  ax-17 1003  ax-4 1005  ax-5o 1007  ax-ext 1494

This theorem depends on definitions:  df-bi 145  df-an 223  df-cleq 1505

Copyright terms: Public domain