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

Theorem eqtrd 2069
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 2048 . 2 (φ → (A = BA = 𝐶))
41, 3mpbid 135 1 (φA = 𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1242
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 1333  ax-gen 1335  ax-4 1397  ax-17 1416  ax-ext 2019
This theorem depends on definitions:  df-bi 110  df-cleq 2030
This theorem is referenced by:  eqtr2d  2070  eqtr3d  2071  eqtr4d  2072  3eqtrd  2073  3eqtrrd  2074  3eqtr2d  2075  syl5eq  2081  syl6eq  2085  rabeqbidv  2546  rabeqbidva  2547  csbidmg  2896  csbco3g  2898  difeq12d  3057  ifeq12d  3341  ifbieq1d  3344  ifbieq2d  3346  ifbieq12d  3348  csbsng  3422  disjpr2  3425  csbunig  3579  iuneq12d  3672  unisn3  4146  op1stbg  4176  opthreg  4234  csbxpg  4364  coeq12d  4443  csbdmg  4472  dmxpinm  4499  xpid11m  4500  reseq12d  4556  csbresg  4558  resima2  4587  imaeq12d  4612  csbrng  4725  opswapg  4750  relcnvtr  4783  relcoi2  4791  relcoi1  4792  iotaint  4823  funprg  4892  funtpg  4893  funcnvres2  4917  fnco  4950  fococnv2  5095  fveq12d  5127  csbfv12g  5152  csbfv2g  5153  csbfvg  5154  dffn5im  5162  funfvdm2  5180  fvun1  5182  fvmpt2d  5200  fvmptt  5205  fndmin  5217  fniniseg2  5232  fnniniseg2  5233  fmptcof  5274  fvresi  5299  fvunsng  5300  fvpr1g  5310  fvpr2g  5311  fvtp1g  5312  funiunfvdm  5345  fcof1o  5372  riotaeqbidv  5414  oveq123d  5476  csbov12g  5486  csbov1g  5487  csbov2g  5488  ovmpt2dxf  5568  caov42d  5629  caovdilemd  5634  caovimo  5636  grprinvd  5638  offval2  5668  caofinvl  5675  ot1stg  5721  ot2ndg  5722  2nd1st  5748  mpt2mptsx  5765  dmmpt2ssx  5767  fmpt2x  5768  fmpt2co  5779  1stconst  5784  tfrexlem  5889  rdgivallem  5908  rdgisuc1  5911  frec0g  5922  frecsuclem1  5926  frecsuclem3  5929  frecrdg  5931  oa0  5976  oasuc  5983  oa1suc  5986  omsuc  5990  nnaass  6003  nndi  6004  nnmass  6005  nnm2  6034  nn2m  6035  ereq1  6049  errn  6064  uniqs2  6102  oviec  6148  ecovass  6151  ecoviass  6152  ecovdi  6153  ecovidi  6154  mulidpi  6302  addasspig  6314  mulasspig  6316  distrpig  6317  indpi  6326  addcmpblnq  6351  mulpipq  6356  dmaddpqlem  6361  nqpi  6362  addcomnqg  6365  recrecnq  6378  ltsonq  6382  ltanqg  6384  ltmnqg  6385  ltaddnq  6390  ltexnqq  6391  archnqq  6400  prarloclemarch  6401  ltrnqg  6403  nq0nn  6424  addcmpblnq0  6425  nqpnq0nq  6435  nqnq0a  6436  nq0m0r  6438  nq0a0  6439  distrnq0  6441  addassnq0  6444  nq02m  6447  prarloclemlo  6476  prarloclemcalc  6484  addnqprllem  6509  addnqprulem  6510  addnqprl  6511  addnqpru  6512  appdivnq  6543  mulnqprl  6548  mulnqpru  6549  addcanprlemu  6588  ltaprlem  6590  ltmprr  6613  cauappcvgprlemladdrl  6628  mulcmpblnrlemg  6648  mulcomsrg  6665  distrsrg  6667  ltsosr  6672  1idsr  6676  00sr  6677  ltasrg  6678  recexgt0sr  6681  elreal2  6708  mulresr  6715  pitonnlem1p1  6722  pitonnlem2  6723  axaddcl  6730  axmulcl  6732  axmulcom  6735  axmulass  6737  axdistr  6738  ax1rid  6741  axcnre  6745  mulid1  6802  mulid2  6803  muladd11  6923  1p1times  6924  readdcan  6930  add42  6950  npcan  6997  addsubass  6998  2addsub  7002  addsubeq4  7003  nppcan  7009  nnpcan  7010  npncan2  7014  nncan  7016  subsub  7017  nnncan  7022  nnncan1  7023  pnpcan2  7027  pnncan  7028  subneg  7036  negneg  7037  negdi2  7045  mul02  7160  mul01  7162  mulneg1  7168  mul2neg  7171  mulm1  7173  ltadd2  7192  rimul  7349  rereim  7350  mulreim  7368  recextlem1  7394  mulcanapd  7404  divcanap1  7422  divrecap2  7430  divcanap4  7438  dividap  7440  divdivdivap  7451  recdivap  7456  divadddivap  7465  divsubdivap  7466  div2negap  7473  divcanap5rd  7554  dmdcanap2d  7557  recgt0  7577  lt2mul2div  7606  nnmulcl  7696  times2  7797  add1p1  7931  sub1m1  7932  cnm2m1cnm3  7933  nn0supp  7990  peano2z  8037  nneoor  8096  cnref1o  8337  rexneg  8493  iooidg  8528  iooval2  8534  icoshftf1o  8609  lincmb01cmp  8621  iccf1o  8622  fzval2  8627  fzsuc  8681  fzpred  8682  fztpval  8695  fseq1p1m1  8706  fzshftral  8720  fzo0to3tp  8825  fzo0sn0fzo1  8827  fzosplitsn  8839  fzosplitprm1  8840  fzisfzounsn  8842  frec2uzsucd  8848  frecuzrdgrrn  8855  frec2uzrdg  8856  frecuzrdglem  8858  frecuzrdgsuc  8862  frecfzennn  8864  iseqeq1  8874  iseqp1  8884  iseqfeq2  8886  iseqfveq  8887  expivallem  8890  expinnval  8892  expp1  8896  expn1ap0  8899  mulexp  8928  expaddzaplem  8932  expaddzap  8933  expmul  8934  expp1zap  8937  expm1ap  8938  sqval  8946  subsq2  8992  binom2  8995  binom21  8996  binom3  8999  zesq  9000  bernneq  9002  imre  9059  crre  9065  remim  9068  reim0b  9070  recj  9075  reneg  9076  readd  9077  resub  9078  remullem  9079  imcj  9083  imneg  9084  imadd  9085  imsub  9086  cjcj  9091  cjadd  9092  ipcnval  9094  cjneg  9098  cjsub  9100  cjexp  9101  imval2  9102  cjap  9114  sqrtsq  9194  absneg  9199  absval2  9201
  Copyright terms: Public domain W3C validator