Theorem eqtr4d 2175

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

Hypotheses

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

Assertion

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

Proof of Theorem eqtr4d

Step	Hyp	Ref	Expression
1		eqtr4d.1	. 2 |- ( ph -> A = B )
2		eqtr4d.2	. . 3 |- ( ph -> C = B )
3	2	eqcomd 2145	. 2 |- ( ph -> B = C )
4	1, 3	eqtrd 2172	1 |- ( ph -> A = C )

Syntax hints:   -> wi 4   = wceq 1331

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 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2121

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

This theorem is referenced by:  3eqtr2d  2178  3eqtr2rd  2179  3eqtr4d  2182  3eqtr4rd  2183  3eqtr4a  2198  sbnfc2  3060  ifsbdc  3486  ifeq1dadc  3502  eqifdc  3506  ifandc  3508  onsucuni2  4479  relop  4689  riinint  4800  iotauni  5100  fniinfv  5479  fsn2  5594  fmptapd  5611  fconst2g  5635  fniunfv  5663  ofres  5996  ofco  6000  frecsuclem  6303  frecrdg  6305  oasuc  6360  nnacom  6380  nnaass  6381  nndi  6382  nnmass  6383  nnmsucr  6384  nnmcom  6385  funresdfunsndc  6402  uniqs2  6489  en1bg  6694  fundmen  6700  1domsn  6713  mapxpen  6742  xpmapenlem  6743  phplem4dom  6756  en2eqpr  6801  sbthlemi5  6849  omp1eomlem  6979  difinfsnlem  6984  ctmlemr  6993  ctssdccl  6996  ctssdc  6998  infnninf  7022  exmidonfinlem  7049  addcmpblnq  7175  distrnqg  7195  ltexnqq  7216  addcmpblnq0  7251  nqnq0a  7262  nqnq0m  7263  nq0m0r  7264  nq0a0  7265  nnanq0  7266  distrnq0  7267  prarloclemlo  7302  prarloclemcalc  7310  genpassl  7332  genpassu  7333  ltsosr  7572  0idsr  7575  1idsr  7576  mulextsr1lem  7588  cnegex  7940  subsub3  7994  subadd4  8006  mulneg12  8159  mulsub  8163  apreap  8349  cru  8364  recextlem1  8412  cju  8719  halfaddsub  8954  nn0supp  9029  nneo  9154  zeo2  9157  uzin  9358  xaddcom  9644  xaddass  9652  xleaddadd  9670  iccf1o  9787  fzsuc2  9859  flqeqceilz  10091  zmod1congr  10114  modqcyc  10132  modqcyc2  10133  modqaddabs  10135  modqmul1  10150  modqaddmulmod  10164  addmodlteq  10171  frec2uzrdg  10182  frecuzrdgsuctlem  10196  seq3val  10231  seqvalcd  10232  seq3fveq2  10242  seq3split  10252  seq3distr  10286  ser0f  10288  expp1  10300  mulexp  10332  mulexpzap  10333  expadd  10335  expaddzap  10337  expmul  10338  expmulzap  10339  expsubap  10341  expdivap  10344  subsq  10399  mulbinom2  10408  binom3  10409  bernneq  10412  nn0opthd  10468  faclbnd  10487  faclbnd6  10490  bccmpl  10500  bcp1n  10507  zfz1isolemiso  10582  seq3coll  10585  shftval2  10598  shftval4  10600  seq3shft  10610  crre  10629  remim  10632  remullem  10643  cjexp  10665  cnrecnv  10682  resqrexlemlo  10785  resqrexlemcalc1  10786  resqrexlemcalc2  10787  resqrexlemcalc3  10788  resqrexlemnm  10790  rsqrmo  10799  abscj  10824  absid  10843  absre  10849  recvalap  10869  maxabsle  10976  maxltsup  10990  2zsupmax  10997  minabs  11007  bdtrilem  11010  bdtri  11011  xrmaxiflemab  11016  xrmaxiflemcom  11018  xrmaxadd  11030  xrbdtri  11045  iooinsup  11046  climaddc1  11098  climmulc2  11100  climsubc1  11101  climsubc2  11102  climcvg1nlem  11118  summodclem3  11149  zsumdc  11153  isum  11154  isumz  11158  isumss  11160  fisumss  11161  fsum3cvg2  11163  fsumadd  11175  isummulc2  11195  sumsplitdc  11201  fsum2dlemstep  11203  fisumcom2  11207  fisum0diag2  11216  fsumconst  11223  telfsumo  11235  fsumparts  11239  fsumrelem  11240  binomlem  11252  isumshft  11259  isumsplit  11260  arisum  11267  arisum2  11268  trireciplem  11269  geolim2  11281  geo2sum  11283  0.999...  11290  cvgratz  11301  mertensabs  11306  clim2prod  11308  prodf1f  11312  prodmodclem2a  11345  ef0lem  11366  efval2  11371  ege2le3  11377  efaddlem  11380  efsub  11387  eftlub  11396  efsep  11397  tanval3ap  11421  efi4p  11424  sinneg  11433  sinmul  11451  sincossq  11455  cos2t  11457  demoivreALT  11480  eirraplem  11483  odd2np1  11570  omoe  11593  divalglemex  11619  divalglemeuneg  11620  divalgmod  11624  flodddiv4  11631  gcdneg  11670  gcdaddm  11672  modgcd  11679  bezoutlemnewy  11684  gcdass  11703  gcdmultiple  11708  algrp1  11727  lcmneg  11755  lcmgcdeq  11764  lcmass  11766  cncongr2  11785  prmexpb  11829  sqrt2irr  11840  2sqpwodd  11854  qnumdenbi  11870  phiprmpw  11898  ctiunctlemfo  11952  strslfv3  12004  restuni2  12346  lmfval  12361  cnfval  12363  cnpfval  12364  txtopon  12431  txcnp  12440  upxp  12441  txrest  12445  cnmptcom  12467  bl2in  12572  xblss2  12574  isxms2  12621  setsmsdsg  12649  setsmstsetg  12650  metss  12663  resubmet  12717  cncfcncntop  12749  dvidlemap  12829  dvcnp2cntop  12832  dvcoapbr  12840  dvcjbr  12841  dvexp  12844  dvexp2  12845  dvrecap  12846  efimpi  12900  tangtx  12919  0nninf  13197  nninfalllemn  13202  trilpolemisumle  13231