Theorem eqtr3d 2242

Description: An equality transitivity equality deduction. (Contributed by NM, 18-Jul-1995.)

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 2213	. 2 |- ( ph -> B = A )
3		eqtr3d.2	. 2 |- ( ph -> A = C )
4	2, 3	eqtrd 2240	1 |- ( ph -> B = C )

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 2189

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

This theorem is referenced by:  3eqtr3d  2248  3eqtr3rd  2249  3eqtr3a  2264  opth  4299  eusvnf  4518  f00  5489  f1imacnv  5561  foimacnv  5562  f1ococnv1  5573  funfvdm  5665  fvmptdf  5690  fndmdif  5708  funopsn  5785  acexmidlemph  5960  acexmidlemab  5961  ovmpodf  6100  fvmpopr2d  6105  oprssov  6111  tfrlemisucaccv  6434  tfr1onlemsucaccv  6450  tfrcllemsucaccv  6463  oav2  6572  omv2  6574  fnsnsplitdc  6614  ecopovtrn  6742  ecopovtrng  6745  map0b  6797  en1  6914  ssenen  6973  fidifsnen  6993  dif1en  7002  undifdc  7047  fidcenumlemr  7083  ordiso2  7163  nninfninc  7251  nnnninfeq2  7257  nninfisollemne  7259  finomni  7268  exmidomni  7270  fodjum  7274  exmidaclem  7351  distrnqg  7535  1qec  7536  prarloclemarch2  7567  nnnq0lem1  7594  nqpnq0nq  7601  distrnq0  7607  prarloclemlt  7641  prmuloclemcalc  7713  ltaprg  7767  prplnqu  7768  recexprlem1ssl  7781  recexprlem1ssu  7782  ltmprr  7790  cauappcvgprlemopl  7794  caucvgprlemopl  7817  caucvgprprlemopl  7845  caucvgprprlemexb  7855  prsrlem1  7890  ltsosr  7912  mulgt0sr  7926  recidpipr  8004  recriota  8038  nntopi  8042  axcaucvglemres  8047  addlid  8246  readdcan  8247  muladd11r  8263  add32r  8267  cnegexlem2  8283  cnegex  8285  pncan2  8314  addsubass  8317  subadd23  8319  addsub12  8320  subid  8326  subid1  8327  npncan  8328  nppcan3  8331  subsub  8337  nppcan2  8338  nnncan2  8344  npncan3  8345  pnpcan  8346  negdi  8364  mvlraddd  8471  mvlladdd  8472  pnpncand  8482  subdi  8492  mulsub  8508  mulsub2  8509  eqord1  8591  recexap  8761  div32ap  8800  divsubdirap  8816  divmuldivap  8820  divdivdivap  8821  divmuleqap  8825  divcanap6  8827  dmdcanap  8830  divsubdivap  8836  div2negap  8843  div2subap  8945  mvllmulapd  8950  prodgt0gt0  8959  cju  9069  zneo  9509  infrenegsupex  9750  qreccl  9798  mul2lt0rlt0  9916  xnpcan  10029  fzosn  10371  modqid  10531  modqm1p1mod0  10557  modqltm1p1mod  10558  modqmul1  10559  modaddmodup  10569  modaddmodlo  10570  modqsubdir  10575  iseqf1olemkle  10679  iseqf1olemklt  10680  seq3f1olemstep  10696  seq3f1oleml  10698  seqf1oglem2  10702  seqfeq3  10711  seq3distr  10714  expineg2  10730  expm1t  10749  expadd  10763  expaddzaplem  10764  expmulzap  10767  sqsubswap  10781  subsq2  10829  binom2sub  10835  binom3  10839  facndiv  10921  bcval5  10945  bcn2p1  10952  bcnm1  10954  pfxccatpfx2  11228  2shfti  11257  shftcan2  11261  reim0  11287  imval2  11320  cjreim2  11330  cjdivap  11335  cnrecnv  11336  rennim  11428  resqrexlemnm  11444  remsqsqrt  11458  sqrtdiv  11468  sqrtmsq  11471  sqabsadd  11481  sqabssub  11482  absreim  11494  absdivap  11496  absnid  11499  sqabs  11508  abslt  11514  absle  11515  recvalap  11523  abssub  11527  maxabslemlub  11633  infxrnegsupex  11689  mulcn2  11738  reccn2ap  11739  cjcn2  11742  summodclem3  11806  summodclem2a  11807  summodc  11809  zsumdc  11810  fsum3  11813  fisumss  11818  fsumcl2lem  11824  fsumm1  11842  fsum1p  11844  isummulc2  11852  telfsumo  11892  binomlem  11909  bcxmas  11915  arisum  11924  trireciplem  11926  trirecip  11927  geolim2  11938  georeclim  11939  cvgratnnlemfm  11955  cvgratz  11958  mertenslemi1  11961  clim2divap  11966  prodmodclem3  12001  prodmodclem2a  12002  zproddc  12005  fprodseq  12009  fprodssdc  12016  fprod1p  12025  efcan  12102  efexp  12108  efzval  12109  efgt0  12110  eftlub  12116  efltim  12124  resinval  12141  recosval  12142  cosmul  12171  cos2t  12176  cos2tsin  12177  cos01bnd  12184  cos12dec  12194  eirraplem  12203  muldvds1  12242  dvdsexp  12287  oexpneg  12303  divalglemqt  12345  divalglemeunn  12347  divalglemeuneg  12349  divalgmod  12353  flodddiv4t2lthalf  12365  bitsmod  12382  bitsinv1lem  12387  gcdid0  12416  gcdaddm  12420  dvdsgcdidd  12430  rpmulgcd  12462  sqgcd  12465  algcvg  12485  eucalgcvga  12495  eucalg  12496  dvdslcm  12506  lcmeq0  12508  lcmgcd  12515  qredeu  12534  sqnprm  12573  divgcdodd  12580  sqrt2irrlem  12598  sqpweven  12612  2sqpwodd  12613  divnumden  12633  hashdvds  12658  phimullem  12662  eulerthlemrprm  12666  eulerthlemth  12669  odzdvds  12683  pythagtriplem3  12705  pythagtriplem4  12706  pythagtriplem14  12715  pythagtriplem19  12720  pcpremul  12731  pceulem  12732  pcqdiv  12745  pcaddlem  12777  fldivp1  12786  1arithlem4  12804  4sqlem10  12825  mul4sqlem  12831  4sqlem11  12839  4sqlem15  12843  4sqlem16  12844  4sqlem17  12845  ennnfonelemhf1o  12899  strslssd  12994  ressbas2d  13015  ressinbasd  13021  topnidg  13199  lidrideqd  13328  grpidd  13330  grprida  13334  gsumress  13342  ismndd  13384  grpidd2  13488  grpinvid1  13499  grpinvid2  13500  grppnpcan2  13541  grpnpncan  13542  dfgrp3mlem  13545  grpsubpropd2  13552  mhmid  13566  mhmmnd  13567  mulgsubcl  13587  mulgneg  13591  mulgaddcomlem  13596  mulginvinv  13599  mulgdirlem  13604  mulgdir  13605  mulgass  13610  mulgmodid  13612  grpissubg  13645  eqgcpbl  13679  ghmid  13700  ghmmulg  13707  resghm  13711  invghm  13780  gsumfzmptfidmadd  13790  mgptopng  13806  srgisid  13863  ringidss  13906  ringcom  13908  opprsubgg  13961  unitgrp  13993  1rinv  14005  0unit  14006  rhmdvdsr  14052  lringuplu  14073  subrngpropd  14093  subrgpropd  14130  lmod0vs  14198  lmodvsmmulgdi  14200  lmodvneg1  14207  lmodcom  14210  lmodsubvs  14220  lmodsubdir  14222  lmodpropd  14226  lspsnsub  14298  lspsneq0b  14304  lsppropd  14309  rlmscabas  14337  lidlbas  14355  zringmulg  14475  restopnb  14768  txcnmpt  14860  cnmpt1t  14872  blhalf  14995  xmspropd  15064  mspropd  15065  mpomulcn  15153  ivthreinc  15232  limcimolemlt  15251  dvfre  15297  dveflem  15313  dvef  15314  ply1termlem  15329  plymullem1  15335  sin2kpi  15398  cos2kpi  15399  sin2pim  15400  cos2pim  15401  ptolemy  15411  sincosq2sgn  15414  sincosq3sgn  15415  sincosq4sgn  15416  sinq12gt0  15417  tangtx  15425  sincosq1eq  15426  abssinper  15433  sinkpi  15434  relogeftb  15452  relogoprlem  15455  relogexp  15459  mpodvdsmulf1o  15577  mersenne  15584  perfectlem1  15586  perfectlem2  15587  perfect  15588  lgsval2lem  15602  lgsdir2lem4  15623  lgsdirprm  15626  lgsdilem2  15628  gausslemma2dlem7  15660  lgseisenlem4  15665  lgsquadlem1  15669  lgsquadlem2  15670  lgsquad2lem1  15673  lgsquad2lem2  15674  2sqlem4  15710  2sqlem6  15712  2sqlem8  15715  peano3nninf  16146  nninfsel  16156  nninffeq  16159  isomninnlem  16171  cvgcmp2nlemabs  16173  trilpolemlt1  16182  trirec0xor  16186  ismkvnnlem  16193