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  6510  addnqprulem  6511  addnqprl  6512  addnqpru  6513  appdivnq  6542  mulnqprl  6547  mulnqpru  6548  addcanprlemu  6587  ltaprlem  6589  ltmprr  6612  mulcmpblnrlemg  6628  mulcomsrg  6645  distrsrg  6647  ltsosr  6652  1idsr  6656  00sr  6657  ltasrg  6658  recexgt0sr  6661  elreal2  6688  mulresr  6695  pitonnlem1p1  6702  pitonnlem2  6703  axaddcl  6710  axmulcl  6712  axmulcom  6715  axmulass  6717  axdistr  6718  ax1rid  6721  axcnre  6725  mulid1  6782  mulid2  6783  muladd11  6903  1p1times  6904  readdcan  6910  add42  6930  npcan  6977  addsubass  6978  2addsub  6982  addsubeq4  6983  nppcan  6989  nnpcan  6990  npncan2  6994  nncan  6996  subsub  6997  nnncan  7002  nnncan1  7003  pnpcan2  7007  pnncan  7008  subneg  7016  negneg  7017  negdi2  7025  mul02  7140  mul01  7142  mulneg1  7148  mul2neg  7151  mulm1  7153  ltadd2  7172  rimul  7329  rereim  7330  mulreim  7348  recextlem1  7374  mulcanapd  7384  divcanap1  7402  divrecap2  7410  divcanap4  7418  dividap  7420  divdivdivap  7431  recdivap  7436  divadddivap  7445  divsubdivap  7446  div2negap  7453  divcanap5rd  7534  dmdcanap2d  7537  recgt0  7557  lt2mul2div  7586  nnmulcl  7676  times2  7777  add1p1  7911  sub1m1  7912  cnm2m1cnm3  7913  nn0supp  7970  peano2z  8017  nneoor  8076  cnref1o  8317  rexneg  8473  iooidg  8508  iooval2  8514  icoshftf1o  8589  lincmb01cmp  8601  iccf1o  8602  fzval2  8607  fzsuc  8661  fzpred  8662  fztpval  8675  fseq1p1m1  8686  fzshftral  8700  fzo0to3tp  8805  fzo0sn0fzo1  8807  fzosplitsn  8819  fzosplitprm1  8820  fzisfzounsn  8822  frec2uzsucd  8828  frecuzrdgrrn  8835  frec2uzrdg  8836  frecuzrdglem  8838  frecuzrdgsuc  8842  frecfzennn  8844  iseqeq1  8854  iseqp1  8864  iseqfeq2  8866  iseqfveq  8867  expivallem  8870  expinnval  8872  expp1  8876  expn1ap0  8879  mulexp  8908  expaddzaplem  8912  expaddzap  8913  expmul  8914  expp1zap  8917  expm1ap  8918  sqval  8926  subsq2  8972  binom2  8975  binom21  8976  binom3  8979  zesq  8980  bernneq  8982  imre  9039  crre  9045  remim  9048  reim0b  9050  recj  9055  reneg  9056  readd  9057  resub  9058  remullem  9059  imcj  9063  imneg  9064  imadd  9065  imsub  9066  cjcj  9071  cjadd  9072  ipcnval  9074  cjneg  9078  cjsub  9080  cjexp  9081  imval2  9082  cjap  9094
  Copyright terms: Public domain W3C validator