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

Theorem eqtrd 2046
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 2025 . 2 (φ → (A = BA = 𝐶))
41, 3mpbid 135 1 (φA = 𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1224
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 1310  ax-gen 1312  ax-4 1374  ax-17 1393  ax-ext 1996
This theorem depends on definitions:  df-bi 110  df-cleq 2007
This theorem is referenced by:  eqtr2d  2047  eqtr3d  2048  eqtr4d  2049  3eqtrd  2050  3eqtrrd  2051  3eqtr2d  2052  syl5eq  2058  syl6eq  2062  rabeqbidv  2522  rabeqbidva  2523  csbidmg  2871  csbco3g  2873  difeq12d  3032  ifeq12d  3314  ifbieq1d  3317  ifbieq2d  3319  ifbieq12d  3321  csbsng  3395  disjpr2  3398  csbunig  3552  iuneq12d  3645  unisn3  4119  op1stbg  4149  opthreg  4207  csbxpg  4337  coeq12d  4416  csbdmg  4445  dmxpinm  4472  xpid11m  4473  reseq12d  4529  csbresg  4531  resima2  4560  imaeq12d  4585  csbrng  4698  opswapg  4723  relcnvtr  4756  relcoi2  4764  relcoi1  4765  iotaint  4796  funprg  4864  funtpg  4865  funcnvres2  4889  fnco  4922  fococnv2  5066  fveq12d  5098  csbfv12g  5123  csbfv2g  5124  csbfvg  5125  dffn5im  5133  funfvdm2  5151  fvun1  5153  fvmpt2d  5171  fvmptt  5176  fndmin  5188  fniniseg2  5203  fnniniseg2  5204  fmptcof  5245  fvresi  5270  fvunsng  5271  fvpr1g  5281  fvpr2g  5282  fvtp1g  5283  funiunfvdm  5316  fcof1o  5343  riotaeqbidv  5385  oveq123d  5446  csbov12g  5456  csbov1g  5457  csbov2g  5458  ovmpt2dxf  5538  caov42d  5599  caovdilemd  5604  caovimo  5606  grprinvd  5608  offval2  5638  caofinvl  5645  ot1stg  5691  ot2ndg  5692  2nd1st  5718  mpt2mptsx  5735  dmmpt2ssx  5737  fmpt2x  5738  fmpt2co  5749  1stconst  5754  tfrexlem  5859  rdgi0g  5875  rdgivallem  5877  rdgisuc1  5880  frecsuclem1  5892  frecsuclem3  5895  frecrdg  5897  oa0  5941  om0  5942  oei0  5943  oasuc  5948  oa1suc  5951  omsuc  5955  nnaass  5968  nndi  5969  nnmass  5970  nnm2  5998  nn2m  5999  ereq1  6013  errn  6028  uniqs2  6066  oviec  6112  ecovass  6115  ecoviass  6116  ecovdi  6117  ecovidi  6118  mulidpi  6165  addasspig  6177  mulasspig  6179  distrpig  6180  addcmpblnq  6213  mulpipq  6218  dmaddpqlem  6223  nqpi  6224  addcomnqg  6227  recrecnq  6240  ltsonq  6244  ltanqg  6246  ltmnqg  6247  ltaddnq  6252  ltexnqq  6253  archnqq  6261  prarloclemarch  6262  ltrnqg  6264  nq0nn  6284  addcmpblnq0  6285  nqpnq0nq  6295  nqnq0a  6296  nq0m0r  6298  nq0a0  6299  distrnq0  6301  addassnq0  6304  nq02m  6306  prarloclemlo  6335  prarloclemcalc  6343  addnqprllem  6369  addnqprulem  6370  addnqprl  6371  addnqpru  6372  appdivnq  6394  mulnqprl  6399  mulnqpru  6400  addcanprlemu  6439  ltaprlem  6441  ltmprr  6464  mulcmpblnrlemg  6479  mulcomsrg  6496  distrsrg  6498  ltsosr  6503  1idsr  6507  00sr  6508  ltasrg  6509  recexgt0sr  6512  elreal2  6538  mulresr  6545  axaddcl  6556  axmulcl  6558  axmulcom  6561  axmulass  6563  axdistr  6564  ax1rid  6567  axcnre  6571  mulid1  6626  mulid2  6627  muladd11  6747  1p1times  6748  readdcan  6754  add42  6774  npcan  6821  addsubass  6822  2addsub  6826  addsubeq4  6827  nppcan  6833  nnpcan  6834  npncan2  6838  nncan  6840  subsub  6841  nnncan  6846  nnncan1  6847  pnpcan2  6851  pnncan  6852  subneg  6860  negneg  6861  negdi2  6869  mul02  6984  mul01  6986  mulneg1  6992  mul2neg  6995  mulm1  6997  ltadd2  7016  rimul  7173  rereim  7174  mulreim  7192  recextlem1  7218  mulcanapd  7228  divcanap1  7246  divrecap2  7254  divcanap4  7262  dividap  7264  divdivdivap  7275  recdivap  7280  divadddivap  7289  divsubdivap  7290  div2negap  7297  divcanap5rd  7378  dmdcanap2d  7381  recgt0  7400  lt2mul2div  7429  nnmulcl  7519  times2  7619  add1p1  7753  sub1m1  7754  cnm2m1cnm3  7755  nn0supp  7809  peano2z  7855  nneoor  7906  rexneg  8220
  Copyright terms: Public domain W3C validator