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

Theorem eqtri 2160
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 2150 . 2  |-  ( A  =  B  <->  A  =  C )
41, 3mpbi 144 1  |-  A  =  C
Colors of variables: wff set class
Syntax hints:    = wceq 1331
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 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2121
This theorem depends on definitions:  df-bi 116  df-cleq 2132
This theorem is referenced by:  eqtr2i  2161  eqtr3i  2162  eqtr4i  2163  3eqtri  2164  3eqtrri  2165  3eqtr2i  2166  cbvrab  2684  csb2  3005  cbvrabcsf  3065  difjust  3072  unjust  3074  injust  3076  dfdif3  3186  difeq12i  3192  inrot  3291  symdif1  3341  rabnc  3395  0in  3398  ssdifin0  3444  dfif3  3487  ifbieq2i  3495  ifbieq12i  3497  pwjust  3511  snjust  3532  dfpr2  3546  disjpr2  3587  difprsn1  3659  diftpsn3  3661  difpr  3662  dfuni2  3738  intab  3800  intunsn  3809  rint0  3810  iunid  3868  viin  3872  iinrabm  3875  2iunin  3879  riin0  3884  iunxprg  3893  unopab  4007  cbvmptf  4022  cbvmpt  4023  unisucg  4336  op1stb  4399  orddif  4462  elxpi  4555  csbxpg  4620  relopabi  4665  inxp  4673  coeq12i  4702  dfdm3  4726  dfrn3  4728  dmun  4746  dmopab  4750  dmopab3  4752  dmxpid  4760  dmxpin  4761  rnopab  4786  rnmpt  4787  rncoss  4809  rncoeq  4812  reseq12i  4817  resundi  4832  resindi  4834  resiun1  4838  resdmdfsn  4862  resopab  4863  mptresid  4873  dfima3  4884  imadisj  4901  ndmima  4916  mptcnv  4941  rnun  4947  rnuni  4950  imaundi  4951  inimass  4955  cnvxp  4957  rnxpm  4968  dminxp  4983  imainrect  4984  cnvcnv3  4988  dmpropg  5011  op1sta  5020  op2ndb  5022  op2nda  5023  resdmres  5030  mptpreima  5032  coundi  5040  coundir  5041  cocnvcnv1  5049  cores2  5051  dfdm2  5073  iotajust  5087  dfiota2  5089  funi  5155  funtp  5176  fntpg  5179  funcnvuni  5192  funcnvres  5196  imadiflem  5202  imadif  5203  imainlem  5204  imain  5205  fnresdisj  5233  mptfng  5248  resdif  5389  fv2  5416  dffv4g  5418  fveq12i  5427  nfvres  5454  0fv  5456  dfimafn2  5471  fnimapr  5481  fvmptss2  5496  fvmptg  5497  fvmpts  5499  fvmpt2  5504  mptfvex  5506  elfvmptrab  5516  fvopab6  5517  f1ompt  5571  dfmpt  5597  ressnop0  5601  fprg  5603  fvsnun1  5617  fsnunfv  5621  fvpr2g  5627  imauni  5662  fliftfuns  5699  cbvriota  5740  oveq123i  5788  fconstmpo  5866  resoprab  5867  mpofun  5873  rnmpo  5881  reldmmpo  5882  ov  5890  ovigg  5891  ovmpt4g  5893  ovg  5909  caov31  5960  elmpocl  5968  f1ocnvd  5972  oprabrexex2  6028  op1st  6044  op2nd  6045  f1stres  6057  f2ndres  6058  unielxp  6072  dfoprab3s  6088  dfoprab4  6090  mpompts  6096  mpofvex  6101  oprab2co  6115  df1st2  6116  df2nd2  6117  f1od2  6132  brtpos0  6149  tposoprab  6177  smores3  6190  tfrlemi14d  6230  tfr1onlemaccex  6245  tfrcllemaccex  6258  rdgisuc1  6281  rdg0  6284  frec0g  6294  df1o2  6326  df2o2  6328  oasuc  6360  omv2  6361  omsuc  6368  ecidsn  6476  qliftfuns  6513  oviec  6535  mapsncnv  6589  dfixp  6594  xpcomco  6720  xpassen  6724  ssenen  6745  undifdc  6812  unfiin  6814  fidcenumlemrks  6841  fidcenumlemr  6843  sbthlemi5  6849  sbthlemi8  6852  fi0  6863  inf00  6918  djuf1olemr  6939  djuinr  6948  djuin  6949  djuun  6952  casefun  6970  casedm  6971  caseinj  6974  caseinl  6976  caseinr  6977  endjusym  6981  eninl  6982  eninr  6983  djudm  6990  djuinj  6991  fodjuomni  7021  fodjumkv  7034  pm54.43  7051  exmidfodomrlemim  7062  xp2dju  7076  djucomen  7077  djuassen  7078  xpdjuen  7079  addpiord  7136  mulpiord  7137  dmaddpi  7145  dmmulpi  7146  recmulnqg  7211  1lt2nq  7226  halfnqq  7230  dfmq0qs  7249  dfplq0qs  7250  genpdf  7328  1prl  7375  1pru  7376  ltexprlemell  7418  ltexprlemelu  7419  recexprlemell  7442  recexprlemelu  7443  cauappcvgprlemm  7465  cauappcvgprlemopl  7466  cauappcvgprlemlol  7467  cauappcvgprlemopu  7468  cauappcvgprlemupu  7469  cauappcvgprlemdisj  7471  cauappcvgprlemloc  7472  cauappcvgprlemladdfu  7474  cauappcvgprlemladdfl  7475  cauappcvgprlemladdrl  7477  cauappcvgprlem2  7480  caucvgprlemm  7488  caucvgprlemopl  7489  caucvgprlemlol  7490  caucvgprlemopu  7491  caucvgprlemupu  7492  caucvgprlemdisj  7494  caucvgprlemloc  7495  caucvgprlemcl  7496  caucvgprlemladdfu  7497  caucvgprlemladdrl  7498  caucvgprlem2  7500  caucvgprprlemell  7505  caucvgprprlemelu  7506  caucvgprprlemml  7514  caucvgprprlemmu  7515  caucvgprprlemclphr  7525  caucvgprprlemexbt  7526  caucvgprprlem2  7530  addsrpr  7565  mulsrpr  7566  caucvgsrlemoffres  7620  caucvgsr  7622  suplocsrlempr  7627  addcnsr  7654  mulcnsr  7655  mulresr  7658  addvalex  7664  pitonnlem1  7665  axi2m1  7695  axcnre  7701  mulcomli  7785  mnfnre  7820  addcomli  7919  add42i  7940  mvrraddi  7991  neg0  8020  negdii  8058  negsubdi2i  8060  crap0  8728  2t2e4  8886  3t2e6  8888  3t3e9  8889  4t2e8  8890  neg1mulneg1e1  8944  8th4div3  8951  halfpm6th  8952  iap0  8955  dfdec10  9197  deceq12i  9202  numltc  9219  decsuc  9224  decsucc  9234  nummac  9238  numma2c  9239  numadd  9240  numaddc  9241  nummul1c  9242  nummul2c  9243  decma  9244  decmac  9245  decma2c  9246  decadd  9247  decaddc  9248  decrmanc  9250  decrmac  9251  decaddci  9254  decsubi  9256  decmul1  9257  decmul1c  9258  decmul2c  9259  11multnc  9261  4t3lem  9290  6t2e12  9297  7t2e14  9302  8t2e16  9308  9t2e18  9315  9t11e99  9323  halfthird  9336  5recm6rec  9337  divfnzn  9425  xnegpnf  9623  xneg0  9626  xaddmnf1  9643  xaddmnf2  9644  mnfaddpnf  9646  iooval2  9710  dfioo2  9769  fzval2  9805  fzsuc2  9871  fztpval  9875  fzo01  10005  fzo12sn  10006  fzo0to42pr  10009  fldiv4p1lem1div2  10090  intqfrac2  10104  intfracq  10105  1tonninf  10225  neg1sqe1  10399  sq2  10400  sq3  10401  cu2  10403  i2  10405  i3  10406  binom2i  10413  sq10  10471  3dec  10473  facp1  10488  fac2  10489  fac4  10491  4bc2eq6  10532  hashp1i  10568  pr0hash2ex  10573  hashfzo  10580  hashxp  10584  zfz1isolem1  10595  cji  10686  cnrecnv  10694  sqrt0  10788  resqrexlemover  10794  resqrexlemcalc3  10800  absi  10843  absimle  10868  sumeq12i  11146  summodclem2a  11162  summodc  11164  sum0  11169  fsumsplitf  11189  fsum2dlemstep  11215  fsumabs  11246  fsumiun  11258  0.999...  11302  mertenslem2  11317  prodeq12i  11344  prodmodc  11359  ege2le3  11389  eft0val  11411  cos0  11448  cos1bnd  11477  cos2bnd  11478  3dvdsdec  11573  3dvds2dec  11574  odd2np1  11581  opoe  11603  nn0o  11615  gcd0val  11660  6gcd4e2  11694  3lcm2e6woprm  11778  3lcm2e6  11849  nn0gcdsq  11889  phiprmpw  11909  phimullem  11912  unennn  11921  ennnfonelemj0  11925  ennnfonelem0  11929  ennnfonelem1  11931  ennnfonelemhf1o  11937  ennnfonelemrn  11943  ennnfonelemdm  11944  strnfvnd  11993  slotslfn  11999  setsfun  12008  setsfun0  12009  setscom  12013  setsslid  12023  2strstr1g  12076  cnco  12404  txuni2  12439  txbas  12441  uptx  12457  txcn  12458  cnmptid  12464  cnmpt2t  12476  xmetxp  12690  cnmetdval  12712  remetdval  12722  resubmet  12731  rerestcntop  12733  divcnap  12738  cnrehmeocntop  12776  dvexp  12858  sinhalfpilem  12894  cosneghalfpi  12901  efhalfpi  12902  cospi  12903  efipi  12904  eulerid  12905  sin2pi  12906  cos2pi  12907  ef2pi  12908  sincosq4sgn  12932  cosq14gt0  12935  tangtx  12941  sincos4thpi  12943  sincos6thpi  12945  sinkpi  12950  cosq34lt1  12953  dfrelog  12961  ex-fl  12996  ex-exp  12998  ex-fac  12999  ex-bc  13000  ex-dvds  13001  ex-gcd  13002  bj-dfom  13190  pwle2  13252  exmid1stab  13254  nninfsellemqall  13272  isomninnlem  13286  taupi  13305
  Copyright terms: Public domain W3C validator