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

Theorem eqtri 2103
Description: An equality transitivity inference. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
eqtri.1  |-  A  =  B
eqtri.2  |-  B  =  C
Assertion
Ref Expression
eqtri  |-  A  =  C

Proof of Theorem eqtri
StepHypRef Expression
1 eqtri.1 . 2  |-  A  =  B
2 eqtri.2 . . 3  |-  B  =  C
32eqeq2i 2093 . 2  |-  ( A  =  B  <->  A  =  C )
41, 3mpbi 143 1  |-  A  =  C
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 2065
This theorem depends on definitions:  df-bi 115  df-cleq 2076
This theorem is referenced by:  eqtr2i  2104  eqtr3i  2105  eqtr4i  2106  3eqtri  2107  3eqtrri  2108  3eqtr2i  2109  cbvrab  2608  csb2  2920  cbvrabcsf  2977  difjust  2984  unjust  2986  injust  2988  dfdif3  3093  difeq12i  3099  inrot  3198  symdif1  3246  rabnc  3294  ssdifin0  3341  dfif3  3382  ifbieq2i  3390  ifbieq12i  3392  pwjust  3402  snjust  3422  dfpr2  3436  disjpr2  3475  difprsn1  3545  diftpsn3  3547  difpr  3548  dfuni2  3624  intab  3686  intunsn  3695  rint0  3696  iunid  3754  viin  3758  iinrabm  3761  2iunin  3765  riin0  3770  unopab  3878  cbvmpt  3893  unisucg  4198  op1stb  4256  orddif  4319  elxpi  4408  csbxpg  4468  relopabi  4512  inxp  4519  coeq12i  4548  dfdm3  4571  dfrn3  4573  dmun  4591  dmopab  4595  dmopab3  4597  rnopab  4630  rnmpt  4631  rncoss  4651  rncoeq  4654  reseq12i  4659  resundi  4674  resindi  4676  resiun1  4679  resdmdfsn  4702  resopab  4703  mptresid  4711  dfima3  4722  imadisj  4738  ndmima  4753  rnun  4783  rnuni  4786  imaundi  4787  inimass  4791  cnvxp  4793  rnxpm  4803  dminxp  4816  imainrect  4817  cnvcnv3  4821  dmpropg  4844  op1sta  4853  op2ndb  4855  op2nda  4856  resdmres  4863  mptpreima  4865  coundi  4873  coundir  4874  cocnvcnv1  4882  cores2  4884  dfdm2  4903  iotajust  4917  dfiota2  4919  funi  4983  funtp  5004  fntpg  5007  funcnvuni  5020  funcnvres  5024  imadiflem  5030  imadif  5031  imainlem  5032  imain  5033  fnresdisj  5061  mptfng  5076  resdif  5200  fv2  5225  dffv4g  5227  fveq12i  5235  nfvres  5259  0fv  5261  dfimafn2  5276  fnimapr  5286  fvmptss2  5300  fvmptg  5301  fvmpts  5303  fvmpt2  5307  mptfvex  5309  fvopab6  5317  f1ompt  5373  dfmpt  5393  ressnop0  5397  fprg  5399  fvsnun1  5413  fsnunfv  5416  fvpr2g  5421  imauni  5453  fliftfuns  5490  cbvriota  5530  oveq123i  5578  resoprab  5649  mpt2fun  5655  rnmpt2  5663  reldmmpt2  5664  ov  5672  ovigg  5673  ovmpt4g  5675  ovg  5691  caov31  5742  elmpt2cl  5750  f1ocnvd  5754  oprabrexex2  5809  op1st  5825  op2nd  5826  f1stres  5838  f2ndres  5839  unielxp  5852  dfoprab3s  5868  dfoprab4  5870  mpt2mpts  5876  mpt2fvex  5881  oprab2co  5891  df1st2  5892  df2nd2  5893  f1od2  5908  brtpos0  5922  tposoprab  5950  smores3  5963  tfrlemi14d  6003  tfr1onlemaccex  6018  tfrcllemaccex  6031  rdgisuc1  6054  rdg0  6057  frec0g  6067  df1o2  6098  df2o2  6100  oasuc  6129  omv2  6130  omsuc  6137  ecidsn  6241  qliftfuns  6278  oviec  6300  xpcomco  6392  xpassen  6396  undifdc  6469  unfiin  6471  inf00  6539  pm54.43  6554  addpiord  6604  mulpiord  6605  dmaddpi  6613  dmmulpi  6614  recmulnqg  6679  1lt2nq  6694  halfnqq  6698  dfmq0qs  6717  dfplq0qs  6718  genpdf  6796  1prl  6843  1pru  6844  ltexprlemell  6886  ltexprlemelu  6887  recexprlemell  6910  recexprlemelu  6911  cauappcvgprlemm  6933  cauappcvgprlemopl  6934  cauappcvgprlemlol  6935  cauappcvgprlemopu  6936  cauappcvgprlemupu  6937  cauappcvgprlemdisj  6939  cauappcvgprlemloc  6940  cauappcvgprlemladdfu  6942  cauappcvgprlemladdfl  6943  cauappcvgprlemladdrl  6945  cauappcvgprlem2  6948  caucvgprlemm  6956  caucvgprlemopl  6957  caucvgprlemlol  6958  caucvgprlemopu  6959  caucvgprlemupu  6960  caucvgprlemdisj  6962  caucvgprlemloc  6963  caucvgprlemcl  6964  caucvgprlemladdfu  6965  caucvgprlemladdrl  6966  caucvgprlem2  6968  caucvgprprlemell  6973  caucvgprprlemelu  6974  caucvgprprlemml  6982  caucvgprprlemmu  6983  caucvgprprlemclphr  6993  caucvgprprlemexbt  6994  caucvgprprlem2  6998  addsrpr  7020  mulsrpr  7021  caucvgsrlemoffres  7074  caucvgsr  7076  addcnsr  7100  mulcnsr  7101  mulresr  7104  addvalex  7110  pitonnlem1  7111  axi2m1  7139  axcnre  7145  mulcomli  7224  mnfnre  7259  addcomli  7356  add42i  7377  mvrraddi  7428  neg0  7457  negdii  7495  negsubdi2i  7497  crap0  8138  2t2e4  8289  3t2e6  8291  3t3e9  8292  4t2e8  8293  neg1mulneg1e1  8346  8th4div3  8353  halfpm6th  8354  iap0  8357  dfdec10  8597  deceq12i  8602  numltc  8619  decsuc  8624  decsucc  8634  nummac  8638  numma2c  8639  numadd  8640  numaddc  8641  nummul1c  8642  nummul2c  8643  decma  8644  decmac  8645  decma2c  8646  decadd  8647  decaddc  8648  decrmanc  8650  decrmac  8651  decaddci  8654  decsubi  8656  decmul1  8657  decmul1c  8658  decmul2c  8659  11multnc  8661  4t3lem  8690  6t2e12  8697  7t2e14  8702  8t2e16  8708  9t2e18  8715  9t11e99  8723  divfnzn  8823  xnegpnf  9007  xneg0  9010  iooval2  9050  dfioo2  9109  fzval2  9144  fzsuc2  9208  fztpval  9212  fzo01  9338  fzo12sn  9339  fzo0to42pr  9342  fldiv4p1lem1div2  9423  intqfrac2  9437  intfracq  9438  neg1sqe1  9703  sq2  9704  sq3  9705  cu2  9706  i2  9708  i3  9709  binom2i  9716  sq10  9773  3dec  9775  facp1  9790  fac2  9791  fac4  9793  4bc2eq6  9834  hashp1i  9870  pr0hash2ex  9875  hashfzo  9882  hashxp  9886  cji  9974  cnrecnv  9982  sqrt0  10075  resqrexlemover  10081  resqrexlemcalc3  10087  absi  10130  absimle  10155  3dvdsdec  10456  3dvds2dec  10457  odd2np1  10464  opoe  10486  nn0o  10498  gcd0val  10543  6gcd4e2  10575  3lcm2e6woprm  10659  3lcm2e6  10730  nn0gcdsq  10769  phiprmpw  10789  phimullem  10792  unennn  10801  ex-fl  10807  ex-fac  10809  ex-bc  10810  ex-dvds  10811  ex-gcd  10812  bj-dfom  10979
  Copyright terms: Public domain W3C validator