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

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

Proof of Theorem eqtr4i
StepHypRef Expression
1 eqtr4i.1 . 2  |-  A  =  B
2 eqtr4i.2 . . 3  |-  C  =  B
32eqcomi 2060 . 2  |-  B  =  C
41, 3eqtri 2076 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:  3eqtr2i  2082  3eqtr2ri  2083  3eqtr4i  2086  3eqtr4ri  2087  rabab  2592  cbvralcsf  2936  cbvrexcsf  2937  cbvrabcsf  2939  dfin5  2953  dfdif2  2954  uneqin  3216  unrab  3236  inrab  3237  inrab2  3238  difrab  3239  dfrab3ss  3243  rabun2  3244  difidALT  3321  difdifdirss  3335  dfif3  3371  tpidm  3500  dfint2  3645  iunrab  3732  uniiun  3738  intiin  3739  0iin  3743  mptv  3881  xpundi  4424  xpundir  4425  resiun2  4659  resopab  4680  opabresid  4687  dfse2  4726  cnvun  4757  cnvin  4759  imaundir  4765  imainrect  4794  cnvcnv2  4802  cnvcnvres  4812  dmtpop  4824  rnsnopg  4827  rnco2  4856  dmco  4857  co01  4863  unidmrn  4878  dfdm2  4880  funimaexg  5011  dfmpt3  5049  mptun  5057  funcocnv2  5179  fnasrn  5369  fnasrng  5371  fpr  5373  fmptap  5381  riotav  5501  dmoprab  5613  rnoprab2  5616  mpt2v  5622  mpt2mptx  5623  abrexex2g  5775  abrexex2  5779  1stval2  5810  2ndval2  5811  fo1st  5812  fo2nd  5813  xp2  5827  dfoprab4f  5847  fmpt2co  5865  tposmpt2  5927  recsfval  5962  frecfnom  6017  frecsuclem1  6018  frecsuclem2  6020  df2o3  6045  o1p1e2  6079  ecqs  6199  qliftf  6222  erovlem  6229  dmaddpq  6535  dmmulpq  6536  enq0enq  6587  nqprlu  6703  m1p1sr  6903  m1m1sr  6904  caucvgsr  6944  dfcnqs  6975  3m1e2  8109  2p2e4  8110  3p2e5  8124  3p3e6  8125  4p2e6  8126  4p3e7  8127  4p4e8  8128  5p2e7  8129  5p3e8  8130  5p4e9  8131  6p2e8  8132  6p3e9  8133  7p2e9  8134  nn0supp  8291  nnzrab  8326  nn0zrab  8327  dec0u  8447  dec0h  8448  decsuc  8457  decsucc  8467  numma  8470  decma  8477  decmac  8478  decma2c  8479  decadd  8480  decaddc  8481  decmul1  8490  decmul1c  8491  decmul2c  8492  5p5e10  8497  6p4e10  8498  7p3e10  8501  8p2e10  8506  5t5e25  8529  6t6e36  8534  8t6e48  8545  nn0uz  8603  nnuz  8604  ioomax  8918  iccmax  8919  ioopos  8920  ioorp  8921  fseq1p1m1  9058  fzo0to2pr  9176  fzo0to3tp  9177  frecfzennn  9367  irec  9518  sq10e99m1  9585  facnn  9595  fac0  9596  faclbnd2  9610  bj-omind  10445
  Copyright terms: Public domain W3C validator