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

Theorem eqtri 2076
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 2066 . 2  |-  ( A  =  B  <->  A  =  C )
41, 3mpbi 137 1  |-  A  =  C
Colors of variables: wff set class
Syntax hints:    = wceq 1259
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-4 1416  ax-17 1435  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-cleq 2049
This theorem is referenced by:  eqtr2i  2077  eqtr3i  2078  eqtr4i  2079  3eqtri  2080  3eqtrri  2081  3eqtr2i  2082  cbvrab  2572  csb2  2881  cbvrabcsf  2938  difjust  2946  unjust  2948  injust  2950  difeq12i  3087  inrot  3179  symdif1  3229  rabnc  3277  ssdifin0  3331  dfif3  3370  ifbieq2i  3378  ifbieq12i  3380  pwjust  3387  snjust  3407  dfpr2  3421  disjpr2  3461  difprsn1  3530  diftpsn3  3532  dfuni2  3609  intab  3671  intunsn  3680  rint0  3681  iunid  3739  viin  3743  iinrabm  3746  2iunin  3750  riin0  3755  unopab  3863  cbvmpt  3878  unisucg  4178  op1stb  4236  orddif  4298  elxpi  4388  csbxpg  4448  relopabi  4490  inxp  4497  coeq12i  4526  dfdm3  4549  dfrn3  4551  dmun  4569  dmopab  4573  dmopab3  4575  rnopab  4608  rnmpt  4609  rncoss  4629  rncoeq  4632  reseq12i  4637  resundi  4652  resindi  4654  resiun1  4657  resopab  4679  mptresid  4687  dfima3  4698  imadisj  4714  ndmima  4729  rnun  4759  rnuni  4762  imaundi  4763  inimass  4767  cnvxp  4769  rnxpm  4779  dminxp  4792  imainrect  4793  cnvcnv3  4797  dmpropg  4820  op1sta  4829  op2ndb  4831  op2nda  4832  resdmres  4839  mptpreima  4841  coundi  4849  coundir  4850  cocnvcnv1  4858  cores2  4860  dfdm2  4879  iotajust  4893  dfiota2  4895  funi  4959  funtp  4979  fntpg  4982  funcnvuni  4995  funcnvres  4999  imadiflem  5005  imadif  5006  imainlem  5007  imain  5008  fnresdisj  5036  mptfng  5051  resdif  5175  fv2  5200  dffv4g  5202  fveq12i  5210  nfvres  5233  0fv  5235  dfimafn2  5250  fnimapr  5260  fvmptss2  5274  fvmptg  5275  fvmpts  5277  fvmpt2  5281  mptfvex  5283  fvopab6  5291  f1ompt  5347  dfmpt  5367  ressnop0  5371  fprg  5373  fvsnun1  5387  fsnunfv  5390  fvpr2g  5395  imauni  5427  fliftfuns  5465  cbvriota  5505  oveq123i  5553  resoprab  5624  mpt2fun  5630  rnmpt2  5638  reldmmpt2  5639  ov  5647  ovigg  5648  ovmpt4g  5650  ovg  5666  caov31  5717  elmpt2cl  5725  f1ocnvd  5729  oprabrexex2  5784  op1st  5800  op2nd  5801  f1stres  5813  f2ndres  5814  unielxp  5827  dfoprab3s  5843  dfoprab4  5845  mpt2mpts  5851  mpt2fvex  5856  oprab2co  5866  df1st2  5867  df2nd2  5868  f1od2  5883  brtpos0  5897  tposoprab  5925  smores3  5938  tfrlemi14d  5977  rdgisuc1  6001  rdg0  6004  frec0g  6013  frecsuc  6021  df1o2  6043  df2o2  6045  oasuc  6074  omv2  6075  omsuc  6081  ecidsn  6183  qliftfuns  6220  oviec  6242  xpcomco  6330  xpassen  6334  addpiord  6471  mulpiord  6472  dmaddpi  6480  dmmulpi  6481  recmulnqg  6546  1lt2nq  6561  halfnqq  6565  dfmq0qs  6584  dfplq0qs  6585  genpdf  6663  1prl  6710  1pru  6711  ltexprlemell  6753  ltexprlemelu  6754  recexprlemell  6777  recexprlemelu  6778  cauappcvgprlemm  6800  cauappcvgprlemopl  6801  cauappcvgprlemlol  6802  cauappcvgprlemopu  6803  cauappcvgprlemupu  6804  cauappcvgprlemdisj  6806  cauappcvgprlemloc  6807  cauappcvgprlemladdfu  6809  cauappcvgprlemladdfl  6810  cauappcvgprlemladdrl  6812  cauappcvgprlem2  6815  caucvgprlemm  6823  caucvgprlemopl  6824  caucvgprlemlol  6825  caucvgprlemopu  6826  caucvgprlemupu  6827  caucvgprlemdisj  6829  caucvgprlemloc  6830  caucvgprlemcl  6831  caucvgprlemladdfu  6832  caucvgprlemladdrl  6833  caucvgprlem2  6835  caucvgprprlemell  6840  caucvgprprlemelu  6841  caucvgprprlemml  6849  caucvgprprlemmu  6850  caucvgprprlemclphr  6860  caucvgprprlemexbt  6861  caucvgprprlem2  6865  addsrpr  6887  mulsrpr  6888  caucvgsrlemoffres  6941  caucvgsr  6943  addcnsr  6967  mulcnsr  6968  mulresr  6971  addvalex  6977  pitonnlem1  6978  axi2m1  7006  axcnre  7012  mulcomli  7091  mnfnre  7126  addcomli  7218  add42i  7239  mvrraddi  7290  neg0  7319  negdii  7357  negsubdi2i  7359  crap0  7985  2t2e4  8136  3t2e6  8138  3t3e9  8139  4t2e8  8140  neg1mulneg1e1  8193  8th4div3  8200  halfpm6th  8201  iap0  8204  dfdec10  8429  deceq12i  8434  numltc  8451  decsuc  8456  decsucc  8466  nummac  8470  numma2c  8471  numadd  8472  numaddc  8473  nummul1c  8474  nummul2c  8475  decma  8476  decmac  8477  decma2c  8478  decadd  8479  decaddc  8480  decrmanc  8482  decrmac  8483  decaddci  8486  decsubi  8488  decmul1  8489  decmul1c  8490  decmul2c  8491  11multnc  8493  4t3lem  8522  6t2e12  8529  7t2e14  8534  8t2e16  8540  9t2e18  8547  9t11e99  8555  divfnzn  8652  xnegpnf  8841  xneg0  8844  iooval2  8884  dfioo2  8943  fzval2  8978  fzsuc2  9042  fztpval  9046  fzo01  9173  fzo12sn  9174  fzo0to42pr  9177  fldiv4p1lem1div2  9249  intqfrac2  9263  intfracq  9264  neg1sqe1  9508  sq2  9509  sq3  9510  cu2  9511  i2  9513  i3  9514  binom2i  9520  sq10  9577  3dec  9579  facp1  9591  fac2  9592  fac4  9594  4bc2eq6  9635  cji  9723  cnrecnv  9731  sqrt0  9823  resqrexlemover  9829  resqrexlemcalc3  9835  absi  9878  absimle  9903  3dvdsdec  10168  3dvds2dec  10169  odd2np1  10176  opoe  10199  nn0o  10211  ex-fl  10251  ex-fac  10253  ex-bc  10254  ex-dvds  10255  bj-dfom  10416
  Copyright terms: Public domain W3C validator