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

Theorem eqtr4di 2228
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 2181 . 2 𝐵 = 𝐶
41, 3eqtrdi 2226 1 (𝜑𝐴 = 𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1353
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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-cleq 2170
This theorem is referenced by:  3eqtr4g  2235  rabxmdc  3454  relop  4773  csbcnvg  4807  dfiun3g  4880  dfiin3g  4881  resima2  4937  relcnvfld  5158  uniabio  5184  fntpg  5268  dffn5im  5557  dfimafn2  5561  fncnvima2  5633  fmptcof  5679  fcoconst  5683  fnasrng  5692  ffnov  5973  fnovim  5977  fnrnov  6014  foov  6015  funimassov  6018  ovelimab  6019  ofc12  6097  caofinvl  6099  dftpos3  6257  tfr0dm  6317  rdgisucinc  6380  oasuc  6459  ecinxp  6604  phplem1  6846  exmidpw  6902  exmidpweq  6903  unfiin  6919  fidcenumlemr  6948  0ct  7100  ctmlemr  7101  exmidaclem  7201  indpi  7332  nqnq0pi  7428  nq0m0r  7446  addnqpr1  7552  recexgt0sr  7763  suplocsrlempr  7797  recidpipr  7846  recidpirq  7848  axrnegex  7869  nntopi  7884  cnref1o  9639  fztp  10064  fseq1m1p1  10081  fz0to4untppr  10110  frecuzrdgrrn  10394  frecuzrdgsuc  10400  frecuzrdgsuctlem  10409  seq3val  10444  seqvalcd  10445  fser0const  10502  mulexpzap  10546  expaddzap  10550  bcp1m1  10729  cjexp  10886  rexuz3  10983  bdtri  11232  climconst  11282  sumfct  11366  zsumdc  11376  fsum3  11379  sum0  11380  fsumcnv  11429  mertenslem2  11528  zproddc  11571  fprodseq  11575  prod0  11577  prod1dc  11578  prodfct  11579  fprodcnv  11617  ef0lem  11652  efzval  11675  efival  11724  sinbnd  11744  cosbnd  11745  eucalgval  12037  eucalginv  12039  eucalglt  12040  eucalgcvga  12041  eucalg  12042  sqpweven  12158  2sqpwodd  12159  dfphi2  12203  phimullem  12208  prmdiv  12218  odzval  12224  pcval  12279  pczpre  12280  pcrec  12291  ennnfonelemhdmp1  12393  ennnfonelemkh  12396  ressinbasd  12515  topnvalg  12648  ismgm  12668  plusffvalg  12673  grpidvalg  12684  issgrp  12701  ismnddef  12711  ismhm  12743  isgrp  12773  grpn0  12798  grpinvfvalg  12805  grpsubfvalg  12808  mulgfvalg  12874  mulgval  12875  mulgnn0p1  12883  iscmn  12923  mgpvalg  12960  issrg  12974  isring  13009  iscrng  13012  opprvalg  13066  istps  13197  cldval  13266  ntrfval  13267  clsfval  13268  neifval  13307  restbasg  13335  tgrest  13336  txval  13422  upxp  13439  uptx  13441  txrest  13443  lmcn2  13447  cnmpt2t  13460  cnmpt2res  13464  imasnopn  13466  psmetxrge0  13499  xmetge0  13532  isxms  13618  isms  13620  bdxmet  13668  qtopbasss  13688  cnblcld  13702  negfcncf  13756  dvfvalap  13817  eldvap  13818  dvidlemap  13827  dvexp2  13843  dvrecap  13844  dveflem  13854  sin0pilem1  13869  ptolemy  13912  coskpi  13936  logbrec  14045  lgslem1  14068  lgsval  14072  lgsval4  14088  lgsfcl3  14089  lgsdilem  14095  lgsdir2lem4  14099  lgsdir2lem5  14100  nninfsellemqall  14420
  Copyright terms: Public domain W3C validator