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

Theorem eqtri 2105
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 2095 . 2  |-  ( A  =  B  <->  A  =  C )
41, 3mpbi 143 1  |-  A  =  C
Colors of variables: wff set class
Syntax hints:    = wceq 1287
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 1379  ax-gen 1381  ax-4 1443  ax-17 1462  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-cleq 2078
This theorem is referenced by:  eqtr2i  2106  eqtr3i  2107  eqtr4i  2108  3eqtri  2109  3eqtrri  2110  3eqtr2i  2111  cbvrab  2613  csb2  2924  cbvrabcsf  2982  difjust  2989  unjust  2991  injust  2993  dfdif3  3099  difeq12i  3105  inrot  3204  symdif1  3253  rabnc  3304  ssdifin0  3351  dfif3  3392  ifbieq2i  3400  ifbieq12i  3402  pwjust  3416  snjust  3436  dfpr2  3450  disjpr2  3489  difprsn1  3559  diftpsn3  3561  difpr  3562  dfuni2  3638  intab  3700  intunsn  3709  rint0  3710  iunid  3768  viin  3772  iinrabm  3775  2iunin  3779  riin0  3784  unopab  3892  cbvmptf  3907  cbvmpt  3908  unisucg  4215  op1stb  4273  orddif  4336  elxpi  4427  csbxpg  4487  relopabi  4531  inxp  4538  coeq12i  4567  dfdm3  4591  dfrn3  4593  dmun  4611  dmopab  4615  dmopab3  4617  rnopab  4650  rnmpt  4651  rncoss  4671  rncoeq  4674  reseq12i  4679  resundi  4694  resindi  4696  resiun1  4699  resdmdfsn  4722  resopab  4723  mptresid  4733  dfima3  4744  imadisj  4761  ndmima  4776  rnun  4806  rnuni  4809  imaundi  4810  inimass  4814  cnvxp  4816  rnxpm  4826  dminxp  4841  imainrect  4842  cnvcnv3  4846  dmpropg  4869  op1sta  4878  op2ndb  4880  op2nda  4881  resdmres  4888  mptpreima  4890  coundi  4898  coundir  4899  cocnvcnv1  4907  cores2  4909  dfdm2  4931  iotajust  4945  dfiota2  4947  funi  5011  funtp  5032  fntpg  5035  funcnvuni  5048  funcnvres  5052  imadiflem  5058  imadif  5059  imainlem  5060  imain  5061  fnresdisj  5089  mptfng  5104  resdif  5238  fv2  5263  dffv4g  5265  fveq12i  5274  nfvres  5300  0fv  5302  dfimafn2  5317  fnimapr  5327  fvmptss2  5342  fvmptg  5343  fvmpts  5345  fvmpt2  5349  mptfvex  5351  fvopab6  5359  f1ompt  5413  dfmpt  5437  ressnop0  5441  fprg  5443  fvsnun1  5457  fsnunfv  5460  fvpr2g  5465  imauni  5501  fliftfuns  5538  cbvriota  5579  oveq123i  5627  resoprab  5698  mpt2fun  5704  rnmpt2  5712  reldmmpt2  5713  ov  5721  ovigg  5722  ovmpt4g  5724  ovg  5740  caov31  5791  elmpt2cl  5799  f1ocnvd  5803  oprabrexex2  5858  op1st  5874  op2nd  5875  f1stres  5887  f2ndres  5888  unielxp  5901  dfoprab3s  5917  dfoprab4  5919  mpt2mpts  5925  mpt2fvex  5930  oprab2co  5940  df1st2  5941  df2nd2  5942  f1od2  5957  brtpos0  5971  tposoprab  5999  smores3  6012  tfrlemi14d  6052  tfr1onlemaccex  6067  tfrcllemaccex  6080  rdgisuc1  6103  rdg0  6106  frec0g  6116  df1o2  6148  df2o2  6150  oasuc  6179  omv2  6180  omsuc  6187  ecidsn  6291  qliftfuns  6328  oviec  6350  mapsncnv  6404  xpcomco  6494  xpassen  6498  ssenen  6519  undifdc  6586  unfiin  6588  sbthlemi5  6614  sbthlemi8  6617  inf00  6670  djuf1olemr  6690  djuinr  6699  casefun  6720  casedm  6721  caseinj  6724  djudm  6729  djuinj  6730  fodjuomni  6748  pm54.43  6762  exmidfodomrlemim  6771  addpiord  6819  mulpiord  6820  dmaddpi  6828  dmmulpi  6829  recmulnqg  6894  1lt2nq  6909  halfnqq  6913  dfmq0qs  6932  dfplq0qs  6933  genpdf  7011  1prl  7058  1pru  7059  ltexprlemell  7101  ltexprlemelu  7102  recexprlemell  7125  recexprlemelu  7126  cauappcvgprlemm  7148  cauappcvgprlemopl  7149  cauappcvgprlemlol  7150  cauappcvgprlemopu  7151  cauappcvgprlemupu  7152  cauappcvgprlemdisj  7154  cauappcvgprlemloc  7155  cauappcvgprlemladdfu  7157  cauappcvgprlemladdfl  7158  cauappcvgprlemladdrl  7160  cauappcvgprlem2  7163  caucvgprlemm  7171  caucvgprlemopl  7172  caucvgprlemlol  7173  caucvgprlemopu  7174  caucvgprlemupu  7175  caucvgprlemdisj  7177  caucvgprlemloc  7178  caucvgprlemcl  7179  caucvgprlemladdfu  7180  caucvgprlemladdrl  7181  caucvgprlem2  7183  caucvgprprlemell  7188  caucvgprprlemelu  7189  caucvgprprlemml  7197  caucvgprprlemmu  7198  caucvgprprlemclphr  7208  caucvgprprlemexbt  7209  caucvgprprlem2  7213  addsrpr  7235  mulsrpr  7236  caucvgsrlemoffres  7289  caucvgsr  7291  addcnsr  7315  mulcnsr  7316  mulresr  7319  addvalex  7325  pitonnlem1  7326  axi2m1  7354  axcnre  7360  mulcomli  7439  mnfnre  7474  addcomli  7571  add42i  7592  mvrraddi  7643  neg0  7672  negdii  7710  negsubdi2i  7712  crap0  8353  2t2e4  8504  3t2e6  8506  3t3e9  8507  4t2e8  8508  neg1mulneg1e1  8561  8th4div3  8568  halfpm6th  8569  iap0  8572  dfdec10  8812  deceq12i  8817  numltc  8834  decsuc  8839  decsucc  8849  nummac  8853  numma2c  8854  numadd  8855  numaddc  8856  nummul1c  8857  nummul2c  8858  decma  8859  decmac  8860  decma2c  8861  decadd  8862  decaddc  8863  decrmanc  8865  decrmac  8866  decaddci  8869  decsubi  8871  decmul1  8872  decmul1c  8873  decmul2c  8874  11multnc  8876  4t3lem  8905  6t2e12  8912  7t2e14  8917  8t2e16  8923  9t2e18  8930  9t11e99  8938  divfnzn  9038  xnegpnf  9222  xneg0  9225  iooval2  9265  dfioo2  9324  fzval2  9359  fzsuc2  9423  fztpval  9427  fzo01  9555  fzo12sn  9556  fzo0to42pr  9559  fldiv4p1lem1div2  9640  intqfrac2  9654  intfracq  9655  1tonninf  9774  neg1sqe1  9948  sq2  9949  sq3  9950  cu2  9951  i2  9953  i3  9954  binom2i  9961  sq10  10018  3dec  10020  facp1  10035  fac2  10036  fac4  10038  4bc2eq6  10079  hashp1i  10115  pr0hash2ex  10120  hashfzo  10127  hashxp  10131  zfz1isolem1  10142  cji  10232  cnrecnv  10240  sqrt0  10333  resqrexlemover  10339  resqrexlemcalc3  10345  absi  10388  absimle  10413  sumeq12i  10646  isummolem2a  10662  isummo  10664  sum0  10668  3dvdsdec  10747  3dvds2dec  10748  odd2np1  10755  opoe  10777  nn0o  10789  gcd0val  10834  6gcd4e2  10866  3lcm2e6woprm  10950  3lcm2e6  11021  nn0gcdsq  11060  phiprmpw  11080  phimullem  11083  unennn  11092  ex-fl  11098  ex-fac  11100  ex-bc  11101  ex-dvds  11102  ex-gcd  11103  bj-dfom  11273  nninfsellemqall  11352
  Copyright terms: Public domain W3C validator