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

Theorem eqtrd 2054
Description: An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
eqtrd.1 (φA = B)
eqtrd.2 (φB = 𝐶)
Assertion
Ref Expression
eqtrd (φA = 𝐶)

Proof of Theorem eqtrd
StepHypRef Expression
1 eqtrd.1 . 2 (φA = B)
2 eqtrd.2 . . 3 (φB = 𝐶)
32eqeq2d 2033 . 2 (φ → (A = BA = 𝐶))
41, 3mpbid 135 1 (φA = 𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1228
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1316  ax-gen 1318  ax-4 1381  ax-17 1400  ax-ext 2004
This theorem depends on definitions:  df-bi 110  df-cleq 2015
This theorem is referenced by:  eqtr2d  2055  eqtr3d  2056  eqtr4d  2057  3eqtrd  2058  3eqtrrd  2059  3eqtr2d  2060  syl5eq  2066  syl6eq  2070  rabeqbidv  2530  rabeqbidva  2531  csbidmg  2879  csbco3g  2881  difeq12d  3040  ifeq12d  3324  ifbieq1d  3327  ifbieq2d  3329  ifbieq12d  3331  csbsng  3405  disjpr2  3408  csbunig  3562  iuneq12d  3655  unisn3  4130  op1stbg  4160  opthreg  4218  csbxpg  4348  coeq12d  4427  csbdmg  4456  dmxpinm  4483  xpid11m  4484  reseq12d  4540  csbresg  4542  resima2  4571  imaeq12d  4596  csbrng  4709  opswapg  4734  relcnvtr  4767  relcoi2  4775  relcoi1  4776  iotaint  4807  funprg  4875  funtpg  4876  funcnvres2  4900  fnco  4933  fococnv2  5077  fveq12d  5109  csbfv12g  5134  csbfv2g  5135  csbfvg  5136  dffn5im  5144  funfvdm2  5162  fvun1  5164  fvmpt2d  5182  fvmptt  5187  fndmin  5199  fniniseg2  5214  fnniniseg2  5215  fmptcof  5256  fvresi  5281  fvunsng  5282  fvpr1g  5292  fvpr2g  5293  fvtp1g  5294  funiunfvdm  5327  fcof1o  5354  riotaeqbidv  5396  oveq123d  5457  csbov12g  5467  csbov1g  5468  csbov2g  5469  ovmpt2dxf  5549  caov42d  5610  caovdilemd  5615  caovimo  5617  grprinvd  5619  offval2  5649  caofinvl  5656  ot1stg  5702  ot2ndg  5703  2nd1st  5729  mpt2mptsx  5746  dmmpt2ssx  5748  fmpt2x  5749  fmpt2co  5760  1stconst  5765  tfrexlem  5870  rdgi0g  5886  rdgivallem  5888  rdgisuc1  5891  frecsuclem1  5903  frecsuclem3  5906  frecrdg  5908  oa0  5952  om0  5953  oei0  5954  oasuc  5959  oa1suc  5962  omsuc  5966  nnaass  5979  nndi  5980  nnmass  5981  nnm2  6009  nn2m  6010  ereq1  6024  errn  6039  uniqs2  6077  oviec  6123  ecovass  6126  ecoviass  6127  ecovdi  6128  ecovidi  6129  mulidpi  6178  addasspig  6190  mulasspig  6192  distrpig  6193  addcmpblnq  6226  mulpipq  6231  dmaddpqlem  6236  nqpi  6237  addcomnqg  6240  recrecnq  6253  ltsonq  6257  ltanqg  6259  ltmnqg  6260  ltaddnq  6265  ltexnqq  6266  archnqq  6274  prarloclemarch  6275  ltrnqg  6277  nq0nn  6297  addcmpblnq0  6298  nqpnq0nq  6308  nqnq0a  6309  nq0m0r  6311  nq0a0  6312  distrnq0  6314  addassnq0  6317  nq02m  6319  prarloclemlo  6348  prarloclemcalc  6356  addnqprllem  6382  addnqprulem  6383  addnqprl  6384  addnqpru  6385  appdivnq  6407  mulnqprl  6412  mulnqpru  6413  addcanprlemu  6452  ltaprlem  6454  mulcmpblnrlemg  6487  mulcomsrg  6504  distrsrg  6506  ltsosr  6511  1idsr  6515  00sr  6516  ltasrg  6517  recexsrlem  6520  elreal2  6542  mulresr  6549  axaddcl  6560  axmulcl  6562  axmulcom  6565  axmulass  6567  axdistr  6568  ax1rid  6571  axcnre  6575  mulid1  6626  mulid2  6627  muladd11  6733  1p1times  6734  readdcan  6740  add42  6760  npcan  6807  addsubass  6808  2addsub  6812  addsubeq4  6813  nppcan  6819  nnpcan  6820  npncan2  6824  nncan  6826  subsub  6827  nnncan  6832  nnncan1  6833  pnpcan2  6837  pnncan  6838  subneg  6846  negneg  6847  negdi2  6855  mul02  6970  mul01  6972  mulneg1  6978  mul2neg  6981  mulm1  6983
  Copyright terms: Public domain W3C validator