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

Theorem eqtr4i 2063
Description: An equality transitivity inference. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
eqtr4i.1 𝐴 = 𝐵
eqtr4i.2 𝐶 = 𝐵
Assertion
Ref Expression
eqtr4i 𝐴 = 𝐶

Proof of Theorem eqtr4i
StepHypRef Expression
1 eqtr4i.1 . 2 𝐴 = 𝐵
2 eqtr4i.2 . . 3 𝐶 = 𝐵
32eqcomi 2044 . 2 𝐵 = 𝐶
41, 3eqtri 2060 1 𝐴 = 𝐶
Colors of variables: wff set class
Syntax hints:   = wceq 1243
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-4 1400  ax-17 1419  ax-ext 2022
This theorem depends on definitions:  df-bi 110  df-cleq 2033
This theorem is referenced by:  3eqtr2i  2066  3eqtr2ri  2067  3eqtr4i  2070  3eqtr4ri  2071  rabab  2575  cbvralcsf  2908  cbvrexcsf  2909  cbvrabcsf  2911  dfin5  2925  dfdif2  2926  uneqin  3188  unrab  3208  inrab  3209  inrab2  3210  difrab  3211  dfrab3ss  3215  rabun2  3216  difidALT  3293  difdifdirss  3307  dfif3  3343  tpidm  3472  dfint2  3617  iunrab  3704  uniiun  3710  intiin  3711  0iin  3715  mptv  3853  xpundi  4396  xpundir  4397  resiun2  4631  resopab  4652  opabresid  4659  dfse2  4698  cnvun  4729  cnvin  4731  imaundir  4737  imainrect  4766  cnvcnv2  4774  cnvcnvres  4784  dmtpop  4796  rnsnopg  4799  rnco2  4828  dmco  4829  co01  4835  unidmrn  4850  dfdm2  4852  funimaexg  4983  dfmpt3  5021  mptun  5029  funcocnv2  5151  fnasrn  5341  fnasrng  5343  fpr  5345  fmptap  5353  riotav  5473  dmoprab  5585  rnoprab2  5588  mpt2v  5594  mpt2mptx  5595  abrexex2g  5747  abrexex2  5751  1stval2  5782  2ndval2  5783  fo1st  5784  fo2nd  5785  xp2  5799  dfoprab4f  5819  fmpt2co  5837  tposmpt2  5896  recsfval  5931  frecfnom  5986  frecsuclem1  5987  frecsuclem2  5989  df2o3  6014  o1p1e2  6048  ecqs  6168  qliftf  6191  erovlem  6198  dmaddpq  6475  dmmulpq  6476  enq0enq  6527  nqprlu  6643  m1p1sr  6843  m1m1sr  6844  caucvgsr  6884  dfcnqs  6915  3m1e2  8034  2p2e4  8035  3p2e5  8050  3p3e6  8051  4p2e6  8052  4p3e7  8053  4p4e8  8054  5p2e7  8055  5p3e8  8056  5p4e9  8057  5p5e10  8058  6p2e8  8059  6p3e9  8060  6p4e10  8061  7p2e9  8062  7p3e10  8063  8p2e10  8064  nn0supp  8232  nnzrab  8267  nn0zrab  8268  dec0u  8380  dec0h  8381  decsuc  8388  decsucc  8392  numma  8396  decma  8403  decmac  8404  decma2c  8405  decadd  8406  decaddc  8407  decmul1c  8412  decmul2c  8413  5t5e25  8441  6t6e36  8446  8t6e48  8457  nn0uz  8505  nnuz  8506  ioomax  8815  iccmax  8816  ioopos  8817  ioorp  8818  fseq1p1m1  8954  fzo0to2pr  9072  fzo0to3tp  9073  frecfzennn  9177  irec  9326  bj-omind  10032
  Copyright terms: Public domain W3C validator