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  6648  m1m1sr  6649  dfcnqs  6698  3m1e2  7774  2p2e4  7775  3p2e5  7790  3p3e6  7791  4p2e6  7792  4p3e7  7793  4p4e8  7794  5p2e7  7795  5p3e8  7796  5p4e9  7797  5p5e10  7798  6p2e8  7799  6p3e9  7800  6p4e10  7801  7p2e9  7802  7p3e10  7803  8p2e10  7804  nn0supp  7970  nnzrab  8005  nn0zrab  8006  dec0u  8118  dec0h  8119  decsuc  8126  decsucc  8130  numma  8134  decma  8141  decmac  8142  decma2c  8143  decadd  8144  decaddc  8145  decmul1c  8150  decmul2c  8151  5t5e25  8179  6t6e36  8184  8t6e48  8195  nn0uz  8243  nnuz  8244  ioomax  8547  iccmax  8548  ioopos  8549  ioorp  8550  fseq1p1m1  8686  fzo0to2pr  8804  fzo0to3tp  8805  frecfzennn  8844  irec  8965  bj-omind  9322
  Copyright terms: Public domain W3C validator