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

Theorem eqtri 2102
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 2092 . 2 (𝐴 = 𝐵𝐴 = 𝐶)
41, 3mpbi 143 1 𝐴 = 𝐶
Colors of variables: wff set class
Syntax hints:   = wceq 1285
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 1377  ax-gen 1379  ax-4 1441  ax-17 1460  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-cleq 2075
This theorem is referenced by:  eqtr2i  2103  eqtr3i  2104  eqtr4i  2105  3eqtri  2106  3eqtrri  2107  3eqtr2i  2108  cbvrab  2600  csb2  2911  cbvrabcsf  2968  difjust  2975  unjust  2977  injust  2979  difeq12i  3089  inrot  3188  symdif1  3236  rabnc  3284  ssdifin0  3331  dfif3  3372  ifbieq2i  3380  ifbieq12i  3382  pwjust  3391  snjust  3411  dfpr2  3425  disjpr2  3464  difprsn1  3533  diftpsn3  3535  dfuni2  3611  intab  3673  intunsn  3682  rint0  3683  iunid  3741  viin  3745  iinrabm  3748  2iunin  3752  riin0  3757  unopab  3865  cbvmpt  3880  unisucg  4177  op1stb  4235  orddif  4298  elxpi  4387  csbxpg  4447  relopabi  4491  inxp  4498  coeq12i  4527  dfdm3  4550  dfrn3  4552  dmun  4570  dmopab  4574  dmopab3  4576  rnopab  4609  rnmpt  4610  rncoss  4630  rncoeq  4633  reseq12i  4638  resundi  4653  resindi  4655  resiun1  4658  resdmdfsn  4681  resopab  4682  mptresid  4690  dfima3  4701  imadisj  4717  ndmima  4732  rnun  4762  rnuni  4765  imaundi  4766  inimass  4770  cnvxp  4772  rnxpm  4782  dminxp  4795  imainrect  4796  cnvcnv3  4800  dmpropg  4823  op1sta  4832  op2ndb  4834  op2nda  4835  resdmres  4842  mptpreima  4844  coundi  4852  coundir  4853  cocnvcnv1  4861  cores2  4863  dfdm2  4882  iotajust  4896  dfiota2  4898  funi  4962  funtp  4983  fntpg  4986  funcnvuni  4999  funcnvres  5003  imadiflem  5009  imadif  5010  imainlem  5011  imain  5012  fnresdisj  5040  mptfng  5055  resdif  5179  fv2  5204  dffv4g  5206  fveq12i  5214  nfvres  5238  0fv  5240  dfimafn2  5255  fnimapr  5265  fvmptss2  5279  fvmptg  5280  fvmpts  5282  fvmpt2  5286  mptfvex  5288  fvopab6  5296  f1ompt  5352  dfmpt  5372  ressnop0  5376  fprg  5378  fvsnun1  5392  fsnunfv  5395  fvpr2g  5400  imauni  5432  fliftfuns  5469  cbvriota  5509  oveq123i  5557  resoprab  5628  mpt2fun  5634  rnmpt2  5642  reldmmpt2  5643  ov  5651  ovigg  5652  ovmpt4g  5654  ovg  5670  caov31  5721  elmpt2cl  5729  f1ocnvd  5733  oprabrexex2  5788  op1st  5804  op2nd  5805  f1stres  5817  f2ndres  5818  unielxp  5831  dfoprab3s  5847  dfoprab4  5849  mpt2mpts  5855  mpt2fvex  5860  oprab2co  5870  df1st2  5871  df2nd2  5872  f1od2  5887  brtpos0  5901  tposoprab  5929  smores3  5942  tfrlemi14d  5982  tfr1onlemaccex  5997  tfrcllemaccex  6010  rdgisuc1  6033  rdg0  6036  frec0g  6046  df1o2  6077  df2o2  6079  oasuc  6108  omv2  6109  omsuc  6116  ecidsn  6219  qliftfuns  6256  oviec  6278  xpcomco  6370  xpassen  6374  undiffi  6443  unfiin  6444  inf00  6503  pm54.43  6518  addpiord  6568  mulpiord  6569  dmaddpi  6577  dmmulpi  6578  recmulnqg  6643  1lt2nq  6658  halfnqq  6662  dfmq0qs  6681  dfplq0qs  6682  genpdf  6760  1prl  6807  1pru  6808  ltexprlemell  6850  ltexprlemelu  6851  recexprlemell  6874  recexprlemelu  6875  cauappcvgprlemm  6897  cauappcvgprlemopl  6898  cauappcvgprlemlol  6899  cauappcvgprlemopu  6900  cauappcvgprlemupu  6901  cauappcvgprlemdisj  6903  cauappcvgprlemloc  6904  cauappcvgprlemladdfu  6906  cauappcvgprlemladdfl  6907  cauappcvgprlemladdrl  6909  cauappcvgprlem2  6912  caucvgprlemm  6920  caucvgprlemopl  6921  caucvgprlemlol  6922  caucvgprlemopu  6923  caucvgprlemupu  6924  caucvgprlemdisj  6926  caucvgprlemloc  6927  caucvgprlemcl  6928  caucvgprlemladdfu  6929  caucvgprlemladdrl  6930  caucvgprlem2  6932  caucvgprprlemell  6937  caucvgprprlemelu  6938  caucvgprprlemml  6946  caucvgprprlemmu  6947  caucvgprprlemclphr  6957  caucvgprprlemexbt  6958  caucvgprprlem2  6962  addsrpr  6984  mulsrpr  6985  caucvgsrlemoffres  7038  caucvgsr  7040  addcnsr  7064  mulcnsr  7065  mulresr  7068  addvalex  7074  pitonnlem1  7075  axi2m1  7103  axcnre  7109  mulcomli  7188  mnfnre  7223  addcomli  7320  add42i  7341  mvrraddi  7392  neg0  7421  negdii  7459  negsubdi2i  7461  crap0  8102  2t2e4  8253  3t2e6  8255  3t3e9  8256  4t2e8  8257  neg1mulneg1e1  8310  8th4div3  8317  halfpm6th  8318  iap0  8321  dfdec10  8561  deceq12i  8566  numltc  8583  decsuc  8588  decsucc  8598  nummac  8602  numma2c  8603  numadd  8604  numaddc  8605  nummul1c  8606  nummul2c  8607  decma  8608  decmac  8609  decma2c  8610  decadd  8611  decaddc  8612  decrmanc  8614  decrmac  8615  decaddci  8618  decsubi  8620  decmul1  8621  decmul1c  8622  decmul2c  8623  11multnc  8625  4t3lem  8654  6t2e12  8661  7t2e14  8666  8t2e16  8672  9t2e18  8679  9t11e99  8687  divfnzn  8787  xnegpnf  8971  xneg0  8974  iooval2  9014  dfioo2  9073  fzval2  9108  fzsuc2  9172  fztpval  9176  fzo01  9302  fzo12sn  9303  fzo0to42pr  9306  fldiv4p1lem1div2  9387  intqfrac2  9401  intfracq  9402  neg1sqe1  9667  sq2  9668  sq3  9669  cu2  9670  i2  9672  i3  9673  binom2i  9680  sq10  9737  3dec  9739  facp1  9754  fac2  9755  fac4  9757  4bc2eq6  9798  sizep1i  9834  pr0size2ex  9839  cji  9927  cnrecnv  9935  sqrt0  10028  resqrexlemover  10034  resqrexlemcalc3  10040  absi  10083  absimle  10108  3dvdsdec  10409  3dvds2dec  10410  odd2np1  10417  opoe  10439  nn0o  10451  gcd0val  10496  6gcd4e2  10528  3lcm2e6woprm  10612  3lcm2e6  10683  unennn  10708  ex-fl  10714  ex-fac  10716  ex-bc  10717  ex-dvds  10718  ex-gcd  10719  bj-dfom  10886
  Copyright terms: Public domain W3C validator