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  ltnnnq  6406  nq0nn  6425  addcmpblnq0  6426  nqpnq0nq  6436  nqnq0a  6437  nq0m0r  6439  nq0a0  6440  distrnq0  6442  addassnq0  6445  nq02m  6448  prarloclemlo  6477  prarloclemcalc  6485  addnqprllem  6510  addnqprulem  6511  addnqprl  6512  addnqpru  6513  appdivnq  6544  mulnqprl  6549  mulnqpru  6550  addcanprlemu  6589  ltaprlem  6591  ltmprr  6614  cauappcvgprlemladdrl  6629  mulcmpblnrlemg  6668  mulcomsrg  6685  distrsrg  6687  ltsosr  6692  1idsr  6696  00sr  6697  ltasrg  6698  recexgt0sr  6701  elreal2  6728  mulresr  6735  pitonnlem1p1  6742  pitonnlem2  6743  axaddcl  6750  axmulcl  6752  axmulcom  6755  axmulass  6757  axdistr  6758  ax1rid  6761  axcnre  6765  mulid1  6822  mulid2  6823  muladd11  6943  1p1times  6944  readdcan  6950  add42  6970  npcan  7017  addsubass  7018  2addsub  7022  addsubeq4  7023  nppcan  7029  nnpcan  7030  npncan2  7034  nncan  7036  subsub  7037  nnncan  7042  nnncan1  7043  pnpcan2  7047  pnncan  7048  subneg  7056  negneg  7057  negdi2  7065  mul02  7180  mul01  7182  mulneg1  7188  mul2neg  7191  mulm1  7193  ltadd2  7212  rimul  7369  rereim  7370  mulreim  7388  recextlem1  7414  mulcanapd  7424  divcanap1  7442  divrecap2  7450  divcanap4  7458  dividap  7460  divdivdivap  7471  recdivap  7476  divadddivap  7485  divsubdivap  7486  div2negap  7493  divcanap5rd  7574  dmdcanap2d  7577  recgt0  7597  lt2mul2div  7626  nnmulcl  7716  times2  7817  add1p1  7951  sub1m1  7952  cnm2m1cnm3  7953  nn0supp  8010  peano2z  8057  nneoor  8116  cnref1o  8357  rexneg  8513  iooidg  8548  iooval2  8554  icoshftf1o  8629  lincmb01cmp  8641  iccf1o  8642  fzval2  8647  fzsuc  8701  fzpred  8702  fztpval  8715  fseq1p1m1  8726  fzshftral  8740  fzo0to3tp  8845  fzo0sn0fzo1  8847  fzosplitsn  8859  fzosplitprm1  8860  fzisfzounsn  8862  frec2uzsucd  8868  frecuzrdgrrn  8875  frec2uzrdg  8876  frecuzrdglem  8878  frecuzrdgsuc  8882  frecfzennn  8884  iseqeq1  8894  iseqp1  8904  iseqfeq2  8906  iseqfveq  8907  expivallem  8910  expinnval  8912  expp1  8916  expn1ap0  8919  mulexp  8948  expaddzaplem  8952  expaddzap  8953  expmul  8954  expp1zap  8957  expm1ap  8958  sqval  8966  subsq2  9012  binom2  9015  binom21  9016  binom3  9019  zesq  9020  bernneq  9022  imre  9079  crre  9085  remim  9088  reim0b  9090  recj  9095  reneg  9096  readd  9097  resub  9098  remullem  9099  imcj  9103  imneg  9104  imadd  9105  imsub  9106  cjcj  9111  cjadd  9112  ipcnval  9114  cjneg  9118  cjsub  9120  cjexp  9121  imval2  9122  cjap  9134  sqrtsq  9214  absneg  9219  absval2  9221
  Copyright terms: Public domain W3C validator