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

Theorem eqtri 2105
Description: An equality transitivity inference. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
eqtri.1 𝐴 = 𝐵
eqtri.2 𝐵 = 𝐶
Assertion
Ref Expression
eqtri 𝐴 = 𝐶

Proof of Theorem eqtri
StepHypRef Expression
1 eqtri.1 . 2 𝐴 = 𝐵
2 eqtri.2 . . 3 𝐵 = 𝐶
32eqeq2i 2095 . 2 (𝐴 = 𝐵𝐴 = 𝐶)
41, 3mpbi 143 1 𝐴 = 𝐶
Colors of variables: wff set class
Syntax hints:   = wceq 1287
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1379  ax-gen 1381  ax-4 1443  ax-17 1462  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-cleq 2078
This theorem is referenced by:  eqtr2i  2106  eqtr3i  2107  eqtr4i  2108  3eqtri  2109  3eqtrri  2110  3eqtr2i  2111  cbvrab  2613  csb2  2924  cbvrabcsf  2982  difjust  2989  unjust  2991  injust  2993  dfdif3  3099  difeq12i  3105  inrot  3204  symdif1  3253  rabnc  3304  ssdifin0  3351  dfif3  3392  ifbieq2i  3400  ifbieq12i  3402  pwjust  3416  snjust  3436  dfpr2  3450  disjpr2  3491  difprsn1  3561  diftpsn3  3563  difpr  3564  dfuni2  3640  intab  3702  intunsn  3711  rint0  3712  iunid  3770  viin  3774  iinrabm  3777  2iunin  3781  riin0  3786  unopab  3894  cbvmptf  3909  cbvmpt  3910  unisucg  4217  op1stb  4275  orddif  4338  elxpi  4429  csbxpg  4489  relopabi  4533  inxp  4540  coeq12i  4569  dfdm3  4593  dfrn3  4595  dmun  4613  dmopab  4617  dmopab3  4619  rnopab  4652  rnmpt  4653  rncoss  4673  rncoeq  4676  reseq12i  4681  resundi  4696  resindi  4698  resiun1  4701  resdmdfsn  4724  resopab  4725  mptresid  4735  dfima3  4746  imadisj  4763  ndmima  4778  rnun  4808  rnuni  4811  imaundi  4812  inimass  4816  cnvxp  4818  rnxpm  4828  dminxp  4843  imainrect  4844  cnvcnv3  4848  dmpropg  4871  op1sta  4880  op2ndb  4882  op2nda  4883  resdmres  4890  mptpreima  4892  coundi  4900  coundir  4901  cocnvcnv1  4909  cores2  4911  dfdm2  4933  iotajust  4947  dfiota2  4949  funi  5013  funtp  5034  fntpg  5037  funcnvuni  5050  funcnvres  5054  imadiflem  5060  imadif  5061  imainlem  5062  imain  5063  fnresdisj  5091  mptfng  5106  resdif  5240  fv2  5265  dffv4g  5267  fveq12i  5276  nfvres  5302  0fv  5304  dfimafn2  5319  fnimapr  5329  fvmptss2  5344  fvmptg  5345  fvmpts  5347  fvmpt2  5351  mptfvex  5353  fvopab6  5361  f1ompt  5415  dfmpt  5439  ressnop0  5443  fprg  5445  fvsnun1  5459  fsnunfv  5462  fvpr2g  5467  imauni  5503  fliftfuns  5540  cbvriota  5581  oveq123i  5629  resoprab  5700  mpt2fun  5706  rnmpt2  5714  reldmmpt2  5715  ov  5723  ovigg  5724  ovmpt4g  5726  ovg  5742  caov31  5793  elmpt2cl  5801  f1ocnvd  5805  oprabrexex2  5860  op1st  5876  op2nd  5877  f1stres  5889  f2ndres  5890  unielxp  5903  dfoprab3s  5919  dfoprab4  5921  mpt2mpts  5927  mpt2fvex  5932  oprab2co  5942  df1st2  5943  df2nd2  5944  f1od2  5959  brtpos0  5973  tposoprab  6001  smores3  6014  tfrlemi14d  6054  tfr1onlemaccex  6069  tfrcllemaccex  6082  rdgisuc1  6105  rdg0  6108  frec0g  6118  df1o2  6150  df2o2  6152  oasuc  6181  omv2  6182  omsuc  6189  ecidsn  6293  qliftfuns  6330  oviec  6352  mapsncnv  6406  xpcomco  6496  xpassen  6500  ssenen  6521  undifdc  6588  unfiin  6590  sbthlemi5  6617  sbthlemi8  6620  inf00  6673  djuf1olemr  6693  djuinr  6702  casefun  6723  casedm  6724  caseinj  6727  djudm  6732  djuinj  6733  fodjuomni  6751  pm54.43  6765  exmidfodomrlemim  6774  addpiord  6822  mulpiord  6823  dmaddpi  6831  dmmulpi  6832  recmulnqg  6897  1lt2nq  6912  halfnqq  6916  dfmq0qs  6935  dfplq0qs  6936  genpdf  7014  1prl  7061  1pru  7062  ltexprlemell  7104  ltexprlemelu  7105  recexprlemell  7128  recexprlemelu  7129  cauappcvgprlemm  7151  cauappcvgprlemopl  7152  cauappcvgprlemlol  7153  cauappcvgprlemopu  7154  cauappcvgprlemupu  7155  cauappcvgprlemdisj  7157  cauappcvgprlemloc  7158  cauappcvgprlemladdfu  7160  cauappcvgprlemladdfl  7161  cauappcvgprlemladdrl  7163  cauappcvgprlem2  7166  caucvgprlemm  7174  caucvgprlemopl  7175  caucvgprlemlol  7176  caucvgprlemopu  7177  caucvgprlemupu  7178  caucvgprlemdisj  7180  caucvgprlemloc  7181  caucvgprlemcl  7182  caucvgprlemladdfu  7183  caucvgprlemladdrl  7184  caucvgprlem2  7186  caucvgprprlemell  7191  caucvgprprlemelu  7192  caucvgprprlemml  7200  caucvgprprlemmu  7201  caucvgprprlemclphr  7211  caucvgprprlemexbt  7212  caucvgprprlem2  7216  addsrpr  7238  mulsrpr  7239  caucvgsrlemoffres  7292  caucvgsr  7294  addcnsr  7318  mulcnsr  7319  mulresr  7322  addvalex  7328  pitonnlem1  7329  axi2m1  7357  axcnre  7363  mulcomli  7442  mnfnre  7477  addcomli  7574  add42i  7595  mvrraddi  7646  neg0  7675  negdii  7713  negsubdi2i  7715  crap0  8356  2t2e4  8507  3t2e6  8509  3t3e9  8510  4t2e8  8511  neg1mulneg1e1  8564  8th4div3  8571  halfpm6th  8572  iap0  8575  dfdec10  8815  deceq12i  8820  numltc  8837  decsuc  8842  decsucc  8852  nummac  8856  numma2c  8857  numadd  8858  numaddc  8859  nummul1c  8860  nummul2c  8861  decma  8862  decmac  8863  decma2c  8864  decadd  8865  decaddc  8866  decrmanc  8868  decrmac  8869  decaddci  8872  decsubi  8874  decmul1  8875  decmul1c  8876  decmul2c  8877  11multnc  8879  4t3lem  8908  6t2e12  8915  7t2e14  8920  8t2e16  8926  9t2e18  8933  9t11e99  8941  divfnzn  9041  xnegpnf  9225  xneg0  9228  iooval2  9268  dfioo2  9327  fzval2  9362  fzsuc2  9426  fztpval  9430  fzo01  9558  fzo12sn  9559  fzo0to42pr  9562  fldiv4p1lem1div2  9643  intqfrac2  9657  intfracq  9658  1tonninf  9777  neg1sqe1  9951  sq2  9952  sq3  9953  cu2  9954  i2  9956  i3  9957  binom2i  9964  sq10  10021  3dec  10023  facp1  10038  fac2  10039  fac4  10041  4bc2eq6  10082  hashp1i  10118  pr0hash2ex  10123  hashfzo  10130  hashxp  10134  zfz1isolem1  10145  cji  10235  cnrecnv  10243  sqrt0  10336  resqrexlemover  10342  resqrexlemcalc3  10348  absi  10391  absimle  10416  sumeq12i  10649  isummolem2a  10665  isummo  10667  sum0  10671  fsumsplitf  10690  3dvdsdec  10771  3dvds2dec  10772  odd2np1  10779  opoe  10801  nn0o  10813  gcd0val  10858  6gcd4e2  10890  3lcm2e6woprm  10974  3lcm2e6  11045  nn0gcdsq  11084  phiprmpw  11104  phimullem  11107  unennn  11116  ex-fl  11122  ex-fac  11124  ex-bc  11125  ex-dvds  11126  ex-gcd  11127  bj-dfom  11297  nninfsellemqall  11376
  Copyright terms: Public domain W3C validator