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

Theorem eqtri 2138
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 2128 . 2  |-  ( A  =  B  <->  A  =  C )
41, 3mpbi 144 1  |-  A  =  C
Colors of variables: wff set class
Syntax hints:    = wceq 1316
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1408  ax-gen 1410  ax-4 1472  ax-17 1491  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-cleq 2110
This theorem is referenced by:  eqtr2i  2139  eqtr3i  2140  eqtr4i  2141  3eqtri  2142  3eqtrri  2143  3eqtr2i  2144  cbvrab  2658  csb2  2977  cbvrabcsf  3035  difjust  3042  unjust  3044  injust  3046  dfdif3  3156  difeq12i  3162  inrot  3261  symdif1  3311  rabnc  3365  0in  3368  ssdifin0  3414  dfif3  3457  ifbieq2i  3465  ifbieq12i  3467  pwjust  3481  snjust  3502  dfpr2  3516  disjpr2  3557  difprsn1  3629  diftpsn3  3631  difpr  3632  dfuni2  3708  intab  3770  intunsn  3779  rint0  3780  iunid  3838  viin  3842  iinrabm  3845  2iunin  3849  riin0  3854  iunxprg  3863  unopab  3977  cbvmptf  3992  cbvmpt  3993  unisucg  4306  op1stb  4369  orddif  4432  elxpi  4525  csbxpg  4590  relopabi  4635  inxp  4643  coeq12i  4672  dfdm3  4696  dfrn3  4698  dmun  4716  dmopab  4720  dmopab3  4722  dmxpid  4730  dmxpin  4731  rnopab  4756  rnmpt  4757  rncoss  4779  rncoeq  4782  reseq12i  4787  resundi  4802  resindi  4804  resiun1  4808  resdmdfsn  4832  resopab  4833  mptresid  4843  dfima3  4854  imadisj  4871  ndmima  4886  mptcnv  4911  rnun  4917  rnuni  4920  imaundi  4921  inimass  4925  cnvxp  4927  rnxpm  4938  dminxp  4953  imainrect  4954  cnvcnv3  4958  dmpropg  4981  op1sta  4990  op2ndb  4992  op2nda  4993  resdmres  5000  mptpreima  5002  coundi  5010  coundir  5011  cocnvcnv1  5019  cores2  5021  dfdm2  5043  iotajust  5057  dfiota2  5059  funi  5125  funtp  5146  fntpg  5149  funcnvuni  5162  funcnvres  5166  imadiflem  5172  imadif  5173  imainlem  5174  imain  5175  fnresdisj  5203  mptfng  5218  resdif  5357  fv2  5384  dffv4g  5386  fveq12i  5395  nfvres  5422  0fv  5424  dfimafn2  5439  fnimapr  5449  fvmptss2  5464  fvmptg  5465  fvmpts  5467  fvmpt2  5472  mptfvex  5474  elfvmptrab  5484  fvopab6  5485  f1ompt  5539  dfmpt  5565  ressnop0  5569  fprg  5571  fvsnun1  5585  fsnunfv  5589  fvpr2g  5595  imauni  5630  fliftfuns  5667  cbvriota  5708  oveq123i  5756  fconstmpo  5834  resoprab  5835  mpofun  5841  rnmpo  5849  reldmmpo  5850  ov  5858  ovigg  5859  ovmpt4g  5861  ovg  5877  caov31  5928  elmpocl  5936  f1ocnvd  5940  oprabrexex2  5996  op1st  6012  op2nd  6013  f1stres  6025  f2ndres  6026  unielxp  6040  dfoprab3s  6056  dfoprab4  6058  mpompts  6064  mpofvex  6069  oprab2co  6083  df1st2  6084  df2nd2  6085  f1od2  6100  brtpos0  6117  tposoprab  6145  smores3  6158  tfrlemi14d  6198  tfr1onlemaccex  6213  tfrcllemaccex  6226  rdgisuc1  6249  rdg0  6252  frec0g  6262  df1o2  6294  df2o2  6296  oasuc  6328  omv2  6329  omsuc  6336  ecidsn  6444  qliftfuns  6481  oviec  6503  mapsncnv  6557  dfixp  6562  xpcomco  6688  xpassen  6692  ssenen  6713  undifdc  6780  unfiin  6782  fidcenumlemrks  6809  fidcenumlemr  6811  sbthlemi5  6817  sbthlemi8  6820  fi0  6831  inf00  6886  djuf1olemr  6907  djuinr  6916  djuin  6917  djuun  6920  casefun  6938  casedm  6939  caseinj  6942  caseinl  6944  caseinr  6945  endjusym  6949  eninl  6950  eninr  6951  djudm  6958  djuinj  6959  fodjuomni  6989  fodjumkv  7002  pm54.43  7014  exmidfodomrlemim  7025  xp2dju  7039  djucomen  7040  djuassen  7041  xpdjuen  7042  addpiord  7092  mulpiord  7093  dmaddpi  7101  dmmulpi  7102  recmulnqg  7167  1lt2nq  7182  halfnqq  7186  dfmq0qs  7205  dfplq0qs  7206  genpdf  7284  1prl  7331  1pru  7332  ltexprlemell  7374  ltexprlemelu  7375  recexprlemell  7398  recexprlemelu  7399  cauappcvgprlemm  7421  cauappcvgprlemopl  7422  cauappcvgprlemlol  7423  cauappcvgprlemopu  7424  cauappcvgprlemupu  7425  cauappcvgprlemdisj  7427  cauappcvgprlemloc  7428  cauappcvgprlemladdfu  7430  cauappcvgprlemladdfl  7431  cauappcvgprlemladdrl  7433  cauappcvgprlem2  7436  caucvgprlemm  7444  caucvgprlemopl  7445  caucvgprlemlol  7446  caucvgprlemopu  7447  caucvgprlemupu  7448  caucvgprlemdisj  7450  caucvgprlemloc  7451  caucvgprlemcl  7452  caucvgprlemladdfu  7453  caucvgprlemladdrl  7454  caucvgprlem2  7456  caucvgprprlemell  7461  caucvgprprlemelu  7462  caucvgprprlemml  7470  caucvgprprlemmu  7471  caucvgprprlemclphr  7481  caucvgprprlemexbt  7482  caucvgprprlem2  7486  addsrpr  7521  mulsrpr  7522  caucvgsrlemoffres  7576  caucvgsr  7578  suplocsrlempr  7583  addcnsr  7610  mulcnsr  7611  mulresr  7614  addvalex  7620  pitonnlem1  7621  axi2m1  7651  axcnre  7657  mulcomli  7741  mnfnre  7776  addcomli  7875  add42i  7896  mvrraddi  7947  neg0  7976  negdii  8014  negsubdi2i  8016  crap0  8684  2t2e4  8842  3t2e6  8844  3t3e9  8845  4t2e8  8846  neg1mulneg1e1  8900  8th4div3  8907  halfpm6th  8908  iap0  8911  dfdec10  9153  deceq12i  9158  numltc  9175  decsuc  9180  decsucc  9190  nummac  9194  numma2c  9195  numadd  9196  numaddc  9197  nummul1c  9198  nummul2c  9199  decma  9200  decmac  9201  decma2c  9202  decadd  9203  decaddc  9204  decrmanc  9206  decrmac  9207  decaddci  9210  decsubi  9212  decmul1  9213  decmul1c  9214  decmul2c  9215  11multnc  9217  4t3lem  9246  6t2e12  9253  7t2e14  9258  8t2e16  9264  9t2e18  9271  9t11e99  9279  halfthird  9292  5recm6rec  9293  divfnzn  9381  xnegpnf  9579  xneg0  9582  xaddmnf1  9599  xaddmnf2  9600  mnfaddpnf  9602  iooval2  9666  dfioo2  9725  fzval2  9761  fzsuc2  9827  fztpval  9831  fzo01  9961  fzo12sn  9962  fzo0to42pr  9965  fldiv4p1lem1div2  10046  intqfrac2  10060  intfracq  10061  1tonninf  10181  neg1sqe1  10355  sq2  10356  sq3  10357  cu2  10359  i2  10361  i3  10362  binom2i  10369  sq10  10427  3dec  10429  facp1  10444  fac2  10445  fac4  10447  4bc2eq6  10488  hashp1i  10524  pr0hash2ex  10529  hashfzo  10536  hashxp  10540  zfz1isolem1  10551  cji  10642  cnrecnv  10650  sqrt0  10744  resqrexlemover  10750  resqrexlemcalc3  10756  absi  10799  absimle  10824  sumeq12i  11102  summodclem2a  11118  summodc  11120  sum0  11125  fsumsplitf  11145  fsum2dlemstep  11171  fsumabs  11202  fsumiun  11214  0.999...  11258  mertenslem2  11273  ege2le3  11304  eft0val  11326  cos0  11364  cos1bnd  11393  cos2bnd  11394  3dvdsdec  11489  3dvds2dec  11490  odd2np1  11497  opoe  11519  nn0o  11531  gcd0val  11576  6gcd4e2  11610  3lcm2e6woprm  11694  3lcm2e6  11765  nn0gcdsq  11805  phiprmpw  11825  phimullem  11828  unennn  11837  ennnfonelemj0  11841  ennnfonelem0  11845  ennnfonelem1  11847  ennnfonelemhf1o  11853  ennnfonelemrn  11859  ennnfonelemdm  11860  strnfvnd  11906  slotslfn  11912  setsfun  11921  setsfun0  11922  setscom  11926  setsslid  11936  2strstr1g  11989  cnco  12317  txuni2  12352  txbas  12354  uptx  12370  txcn  12371  cnmptid  12377  cnmpt2t  12389  xmetxp  12603  cnmetdval  12625  remetdval  12635  resubmet  12644  rerestcntop  12646  divcnap  12651  cnrehmeocntop  12689  dvexp  12771  sinhalfpilem  12799  cosneghalfpi  12806  efhalfpi  12807  cospi  12808  efipi  12809  eulerid  12810  sin2pi  12811  cos2pi  12812  ef2pi  12813  sincosq4sgn  12837  cosq14gt0  12840  tangtx  12846  sincos4thpi  12848  sincos6thpi  12850  sinkpi  12855  cosq34lt1  12858  ex-fl  12864  ex-exp  12866  ex-fac  12867  ex-bc  12868  ex-dvds  12869  ex-gcd  12870  bj-dfom  13058  pwle2  13120  exmid1stab  13122  nninfsellemqall  13138  isomninnlem  13152  taupi  13166
  Copyright terms: Public domain W3C validator