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

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

Proof of Theorem eqtr4i
StepHypRef Expression
1 eqtr4i.1 . 2 A = B
2 eqtr4i.2 . . 3 𝐶 = B
32eqcomi 2041 . 2 B = 𝐶
41, 3eqtri 2057 1 A = 𝐶
Colors of variables: wff set class
Syntax hints:   = wceq 1242
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 1333  ax-gen 1335  ax-4 1397  ax-17 1416  ax-ext 2019
This theorem depends on definitions:  df-bi 110  df-cleq 2030
This theorem is referenced by:  3eqtr2i  2063  3eqtr2ri  2064  3eqtr4i  2067  3eqtr4ri  2068  rabab  2569  cbvralcsf  2902  cbvrexcsf  2903  cbvrabcsf  2905  dfin5  2919  dfdif2  2920  uneqin  3182  unrab  3202  inrab  3203  inrab2  3204  difrab  3205  dfrab3ss  3209  rabun2  3210  difidALT  3287  difdifdirss  3301  dfif3  3337  tpidm  3463  dfint2  3608  iunrab  3695  uniiun  3701  intiin  3702  0iin  3706  mptv  3844  xpundi  4339  xpundir  4340  resiun2  4574  resopab  4595  opabresid  4602  dfse2  4641  cnvun  4672  cnvin  4674  imaundir  4680  imainrect  4709  cnvcnv2  4717  cnvcnvres  4727  dmtpop  4739  rnsnopg  4742  rnco2  4771  dmco  4772  co01  4778  unidmrn  4793  dfdm2  4795  funimaexg  4926  dfmpt3  4964  mptun  4972  funcocnv2  5094  fnasrn  5284  fnasrng  5286  fpr  5288  fmptap  5296  riotav  5416  dmoprab  5527  rnoprab2  5530  mpt2v  5536  mpt2mptx  5537  abrexex2g  5689  abrexex2  5693  1stval2  5724  2ndval2  5725  fo1st  5726  fo2nd  5727  xp2  5741  dfoprab4f  5761  fmpt2co  5779  tposmpt2  5837  recsfval  5872  frecfnom  5925  frecsuclem1  5926  frecsuclem2  5928  df2o3  5953  o1p1e2  5987  ecqs  6104  qliftf  6127  erovlem  6134  dmaddpq  6363  dmmulpq  6364  enq0enq  6413  m1p1sr  6668  m1m1sr  6669  dfcnqs  6718  3m1e2  7794  2p2e4  7795  3p2e5  7810  3p3e6  7811  4p2e6  7812  4p3e7  7813  4p4e8  7814  5p2e7  7815  5p3e8  7816  5p4e9  7817  5p5e10  7818  6p2e8  7819  6p3e9  7820  6p4e10  7821  7p2e9  7822  7p3e10  7823  8p2e10  7824  nn0supp  7990  nnzrab  8025  nn0zrab  8026  dec0u  8138  dec0h  8139  decsuc  8146  decsucc  8150  numma  8154  decma  8161  decmac  8162  decma2c  8163  decadd  8164  decaddc  8165  decmul1c  8170  decmul2c  8171  5t5e25  8199  6t6e36  8204  8t6e48  8215  nn0uz  8263  nnuz  8264  ioomax  8567  iccmax  8568  ioopos  8569  ioorp  8570  fseq1p1m1  8706  fzo0to2pr  8824  fzo0to3tp  8825  frecfzennn  8864  irec  8985  bj-omind  9368
  Copyright terms: Public domain W3C validator