ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  eqtr4di GIF version

Theorem eqtr4di 2191
Description: An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
eqtr4di.1 (𝜑𝐴 = 𝐵)
eqtr4di.2 𝐶 = 𝐵
Assertion
Ref Expression
eqtr4di (𝜑𝐴 = 𝐶)

Proof of Theorem eqtr4di
StepHypRef Expression
1 eqtr4di.1 . 2 (𝜑𝐴 = 𝐵)
2 eqtr4di.2 . . 3 𝐶 = 𝐵
32eqcomi 2144 . 2 𝐵 = 𝐶
41, 3eqtrdi 2189 1 (𝜑𝐴 = 𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1332
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 1424  ax-gen 1426  ax-4 1488  ax-17 1507  ax-ext 2122
This theorem depends on definitions:  df-bi 116  df-cleq 2133
This theorem is referenced by:  3eqtr4g  2198  rabxmdc  3398  relop  4696  csbcnvg  4730  dfiun3g  4803  dfiin3g  4804  resima2  4860  relcnvfld  5079  uniabio  5105  fntpg  5186  dffn5im  5474  dfimafn2  5478  fncnvima2  5548  fmptcof  5594  fcoconst  5598  fnasrng  5607  ffnov  5882  fnovim  5886  fnrnov  5923  foov  5924  funimassov  5927  ovelimab  5928  ofc12  6009  caofinvl  6011  dftpos3  6166  tfr0dm  6226  rdgisucinc  6289  oasuc  6367  ecinxp  6511  phplem1  6753  exmidpw  6809  unfiin  6821  fidcenumlemr  6850  0ct  6999  ctmlemr  7000  exmidaclem  7080  indpi  7173  nqnq0pi  7269  nq0m0r  7287  addnqpr1  7393  recexgt0sr  7604  suplocsrlempr  7638  recidpipr  7687  recidpirq  7689  axrnegex  7710  nntopi  7725  cnref1o  9468  fztp  9888  fseq1m1p1  9905  frecuzrdgrrn  10211  frecuzrdgsuc  10217  frecuzrdgsuctlem  10226  seq3val  10261  seqvalcd  10262  fser0const  10319  mulexpzap  10363  expaddzap  10367  bcp1m1  10542  cjexp  10696  rexuz3  10793  bdtri  11042  climconst  11090  sumfct  11174  zsumdc  11184  fsum3  11187  sum0  11188  fsumcnv  11237  mertenslem2  11336  zproddc  11379  ef0lem  11401  efzval  11424  efival  11473  sinbnd  11493  cosbnd  11494  eucalgval  11769  eucalginv  11771  eucalglt  11772  eucalgcvga  11773  eucalg  11774  sqpweven  11887  2sqpwodd  11888  dfphi2  11930  phimullem  11935  ennnfonelemhdmp1  11956  ennnfonelemkh  11959  ressid2  12055  ressval2  12056  topnvalg  12169  istps  12236  cldval  12305  ntrfval  12306  clsfval  12307  neifval  12346  restbasg  12374  tgrest  12375  txval  12461  upxp  12478  uptx  12480  txrest  12482  lmcn2  12486  cnmpt2t  12499  cnmpt2res  12503  imasnopn  12505  psmetxrge0  12538  xmetge0  12571  isxms  12657  isms  12659  bdxmet  12707  qtopbasss  12727  cnblcld  12741  negfcncf  12795  dvfvalap  12856  eldvap  12857  dvidlemap  12866  dvexp2  12882  dvrecap  12883  dveflem  12893  sin0pilem1  12908  ptolemy  12951  coskpi  12975  logbrec  13083  nninfsellemqall  13384
  Copyright terms: Public domain W3C validator