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

Theorem eqtr4i 2108
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 2089 . 2 𝐵 = 𝐶
41, 3eqtri 2105 1 𝐴 = 𝐶
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:  3eqtr2i  2111  3eqtr2ri  2112  3eqtr4i  2115  3eqtr4ri  2116  rabab  2634  cbvralcsf  2979  cbvrexcsf  2980  cbvrabcsf  2982  dfin5  2995  dfdif2  2996  uneqin  3239  unrab  3259  inrab  3260  inrab2  3261  difrab  3262  dfrab3ss  3266  rabun2  3267  difidALT  3340  difdifdirss  3354  dfif3  3392  tpidm  3527  dfint2  3673  iunrab  3760  uniiun  3766  intiin  3767  0iin  3771  mptv  3910  xpundi  4462  xpundir  4463  resiun2  4700  resopab  4723  opabresid  4732  dfse2  4772  cnvun  4803  cnvin  4805  imaundir  4811  imainrect  4842  cnvcnv2  4850  cnvcnvres  4860  dmtpop  4872  rnsnopg  4875  rnco2  4904  dmco  4905  co01  4911  unidmrn  4929  dfdm2  4931  funimaexg  5063  dfmpt3  5101  mptun  5109  funcocnv2  5241  fnasrn  5438  fnasrng  5440  fpr  5442  fmptap  5450  riotav  5574  dmoprab  5686  rnoprab2  5689  mpt2v  5695  mpt2mptx  5696  abrexex2g  5848  abrexex2  5852  1stval2  5883  2ndval2  5884  fo1st  5885  fo2nd  5886  xp2  5900  dfoprab4f  5920  fmpt2co  5938  tposmpt2  6000  recsfval  6034  frecfnom  6120  freccllem  6121  frecfcllem  6123  frecsuclem  6125  df2o3  6149  o1p1e2  6183  ecqs  6306  qliftf  6329  erovlem  6336  mapsnf1o3  6406  xpf1o  6512  djuunr  6702  dmaddpq  6882  dmmulpq  6883  enq0enq  6934  nqprlu  7050  m1p1sr  7250  m1m1sr  7251  caucvgsr  7291  dfcnqs  7322  3m1e2  8476  2p2e4  8477  3p2e5  8491  3p3e6  8492  4p2e6  8493  4p3e7  8494  4p4e8  8495  5p2e7  8496  5p3e8  8497  5p4e9  8498  6p2e8  8499  6p3e9  8500  7p2e9  8501  nn0supp  8658  nnzrab  8707  nn0zrab  8708  dec0u  8829  dec0h  8830  decsuc  8839  decsucc  8849  numma  8852  decma  8859  decmac  8860  decma2c  8861  decadd  8862  decaddc  8863  decmul1  8872  decmul1c  8873  decmul2c  8874  5p5e10  8879  6p4e10  8880  7p3e10  8883  8p2e10  8888  5t5e25  8911  6t6e36  8916  8t6e48  8927  nn0uz  8985  nnuz  8986  ioomax  9298  iccmax  9299  ioopos  9300  ioorp  9301  fseq1p1m1  9438  fzo0to2pr  9557  fzo0to3tp  9558  frecfzennn  9761  irec  9952  sq10e99m1  10019  facnn  10032  fac0  10033  faclbnd2  10047  zfz1isolemsplit  10140  minmax  10556  phiprmpw  11080  unennn  11092  bj-omind  11274
  Copyright terms: Public domain W3C validator