Theorem eqtr3d 2231

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

Syntax hints:   -> wi 4   = wceq 1364

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  3eqtr3d  2237  3eqtr3rd  2238  3eqtr3a  2253  opth  4270  eusvnf  4488  f00  5449  f1imacnv  5521  foimacnv  5522  f1ococnv1  5533  funfvdm  5624  fvmptdf  5649  fndmdif  5667  acexmidlemph  5915  acexmidlemab  5916  ovmpodf  6054  fvmpopr2d  6059  oprssov  6065  tfrlemisucaccv  6383  tfr1onlemsucaccv  6399  tfrcllemsucaccv  6412  oav2  6521  omv2  6523  fnsnsplitdc  6563  ecopovtrn  6691  ecopovtrng  6694  map0b  6746  en1  6858  ssenen  6912  fidifsnen  6931  dif1en  6940  undifdc  6985  fidcenumlemr  7021  ordiso2  7101  nninfninc  7189  nnnninfeq2  7195  nninfisollemne  7197  finomni  7206  exmidomni  7208  fodjum  7212  exmidaclem  7275  distrnqg  7454  1qec  7455  prarloclemarch2  7486  nnnq0lem1  7513  nqpnq0nq  7520  distrnq0  7526  prarloclemlt  7560  prmuloclemcalc  7632  ltaprg  7686  prplnqu  7687  recexprlem1ssl  7700  recexprlem1ssu  7701  ltmprr  7709  cauappcvgprlemopl  7713  caucvgprlemopl  7736  caucvgprprlemopl  7764  caucvgprprlemexb  7774  prsrlem1  7809  ltsosr  7831  mulgt0sr  7845  recidpipr  7923  recriota  7957  nntopi  7961  axcaucvglemres  7966  addlid  8165  readdcan  8166  muladd11r  8182  add32r  8186  cnegexlem2  8202  cnegex  8204  pncan2  8233  addsubass  8236  subadd23  8238  addsub12  8239  subid  8245  subid1  8246  npncan  8247  nppcan3  8250  subsub  8256  nppcan2  8257  nnncan2  8263  npncan3  8264  pnpcan  8265  negdi  8283  mvlraddd  8390  mvlladdd  8391  pnpncand  8401  subdi  8411  mulsub  8427  mulsub2  8428  eqord1  8510  recexap  8680  div32ap  8719  divsubdirap  8735  divmuldivap  8739  divdivdivap  8740  divmuleqap  8744  divcanap6  8746  dmdcanap  8749  divsubdivap  8755  div2negap  8762  div2subap  8864  mvllmulapd  8869  prodgt0gt0  8878  cju  8988  zneo  9427  infrenegsupex  9668  qreccl  9716  mul2lt0rlt0  9834  xnpcan  9947  fzosn  10281  modqid  10441  modqm1p1mod0  10467  modqltm1p1mod  10468  modqmul1  10469  modaddmodup  10479  modaddmodlo  10480  modqsubdir  10485  iseqf1olemkle  10589  iseqf1olemklt  10590  seq3f1olemstep  10606  seq3f1oleml  10608  seqf1oglem2  10612  seqfeq3  10621  seq3distr  10624  expineg2  10640  expm1t  10659  expadd  10673  expaddzaplem  10674  expmulzap  10677  sqsubswap  10691  subsq2  10739  binom2sub  10745  binom3  10749  facndiv  10831  bcval5  10855  bcn2p1  10862  bcnm1  10864  2shfti  10996  shftcan2  11000  reim0  11026  imval2  11059  cjreim2  11069  cjdivap  11074  cnrecnv  11075  rennim  11167  resqrexlemnm  11183  remsqsqrt  11197  sqrtdiv  11207  sqrtmsq  11210  sqabsadd  11220  sqabssub  11221  absreim  11233  absdivap  11235  absnid  11238  sqabs  11247  abslt  11253  absle  11254  recvalap  11262  abssub  11266  maxabslemlub  11372  infxrnegsupex  11428  mulcn2  11477  reccn2ap  11478  cjcn2  11481  summodclem3  11545  summodclem2a  11546  summodc  11548  zsumdc  11549  fsum3  11552  fisumss  11557  fsumcl2lem  11563  fsumm1  11581  fsum1p  11583  isummulc2  11591  telfsumo  11631  binomlem  11648  bcxmas  11654  arisum  11663  trireciplem  11665  trirecip  11666  geolim2  11677  georeclim  11678  cvgratnnlemfm  11694  cvgratz  11697  mertenslemi1  11700  clim2divap  11705  prodmodclem3  11740  prodmodclem2a  11741  zproddc  11744  fprodseq  11748  fprodssdc  11755  fprod1p  11764  efcan  11841  efexp  11847  efzval  11848  efgt0  11849  eftlub  11855  efltim  11863  resinval  11880  recosval  11881  cosmul  11910  cos2t  11915  cos2tsin  11916  cos01bnd  11923  cos12dec  11933  eirraplem  11942  muldvds1  11981  dvdsexp  12026  oexpneg  12042  divalglemqt  12084  divalglemeunn  12086  divalglemeuneg  12088  divalgmod  12092  flodddiv4t2lthalf  12104  gcdid0  12147  gcdaddm  12151  dvdsgcdidd  12161  rpmulgcd  12193  sqgcd  12196  algcvg  12216  eucalgcvga  12226  eucalg  12227  dvdslcm  12237  lcmeq0  12239  lcmgcd  12246  qredeu  12265  sqnprm  12304  divgcdodd  12311  sqrt2irrlem  12329  sqpweven  12343  2sqpwodd  12344  divnumden  12364  hashdvds  12389  phimullem  12393  eulerthlemrprm  12397  eulerthlemth  12400  odzdvds  12414  pythagtriplem3  12436  pythagtriplem4  12437  pythagtriplem14  12446  pythagtriplem19  12451  pcpremul  12462  pceulem  12463  pcqdiv  12476  pcaddlem  12508  fldivp1  12517  1arithlem4  12535  4sqlem10  12556  mul4sqlem  12562  4sqlem11  12570  4sqlem15  12574  4sqlem16  12575  4sqlem17  12576  ennnfonelemhf1o  12630  strslssd  12725  ressbas2d  12746  ressinbasd  12752  topnidg  12923  lidrideqd  13024  grpidd  13026  grprida  13030  gsumress  13038  ismndd  13078  grpidd2  13173  grpinvid1  13184  grpinvid2  13185  grppnpcan2  13226  grpnpncan  13227  dfgrp3mlem  13230  grpsubpropd2  13237  mhmid  13245  mhmmnd  13246  mulgsubcl  13266  mulgneg  13270  mulgaddcomlem  13275  mulginvinv  13278  mulgdirlem  13283  mulgdir  13284  mulgass  13289  mulgmodid  13291  grpissubg  13324  eqgcpbl  13358  ghmid  13379  ghmmulg  13386  resghm  13390  invghm  13459  gsumfzmptfidmadd  13469  mgptopng  13485  srgisid  13542  ringidss  13585  ringcom  13587  opprsubgg  13640  unitgrp  13672  1rinv  13684  0unit  13685  rhmdvdsr  13731  lringuplu  13752  subrngpropd  13772  subrgpropd  13809  lmod0vs  13877  lmodvsmmulgdi  13879  lmodvneg1  13886  lmodcom  13889  lmodsubvs  13899  lmodsubdir  13901  lmodpropd  13905  lspsnsub  13977  lspsneq0b  13983  lsppropd  13988  rlmscabas  14016  lidlbas  14034  zringmulg  14154  restopnb  14417  txcnmpt  14509  cnmpt1t  14521  blhalf  14644  xmspropd  14713  mspropd  14714  mpomulcn  14802  ivthreinc  14881  limcimolemlt  14900  dvfre  14946  dveflem  14962  dvef  14963  ply1termlem  14978  plymullem1  14984  sin2kpi  15047  cos2kpi  15048  sin2pim  15049  cos2pim  15050  ptolemy  15060  sincosq2sgn  15063  sincosq3sgn  15064  sincosq4sgn  15065  sinq12gt0  15066  tangtx  15074  sincosq1eq  15075  abssinper  15082  sinkpi  15083  relogeftb  15101  relogoprlem  15104  relogexp  15108  mpodvdsmulf1o  15226  mersenne  15233  perfectlem1  15235  perfectlem2  15236  perfect  15237  lgsval2lem  15251  lgsdir2lem4  15272  lgsdirprm  15275  lgsdilem2  15277  gausslemma2dlem7  15309  lgseisenlem4  15314  lgsquadlem1  15318  lgsquadlem2  15319  lgsquad2lem1  15322  lgsquad2lem2  15323  2sqlem4  15359  2sqlem6  15361  2sqlem8  15364  peano3nninf  15651  nninfsel  15661  nninffeq  15664  isomninnlem  15674  cvgcmp2nlemabs  15676  trilpolemlt1  15685  trirec0xor  15689  ismkvnnlem  15696