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

Theorem eqtr4i 2141
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 2121 . 2  |-  B  =  C
41, 3eqtri 2138 1  |-  A  =  C
Colors of variables: wff set class
Syntax hints:    = wceq 1316
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1408  ax-gen 1410  ax-4 1472  ax-17 1491  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-cleq 2110
This theorem is referenced by:  3eqtr2i  2144  3eqtr2ri  2145  3eqtr4i  2148  3eqtr4ri  2149  rabab  2681  cbvralcsf  3032  cbvrexcsf  3033  cbvrabcsf  3035  dfin5  3048  dfdif2  3049  uneqin  3297  unrab  3317  inrab  3318  inrab2  3319  difrab  3320  dfrab3ss  3324  rabun2  3325  difidALT  3402  difdifdirss  3417  dfif3  3457  tpidm  3595  dfint2  3743  iunrab  3830  uniiun  3836  intiin  3837  0iin  3841  mptv  3995  xpundi  4565  xpundir  4566  resiun2  4809  resopab  4833  opabresid  4842  dfse2  4882  cnvun  4914  cnvin  4916  imaundir  4922  imainrect  4954  cnvcnv2  4962  cnvcnvres  4972  dmtpop  4984  rnsnopg  4987  rnco2  5016  dmco  5017  co01  5023  unidmrn  5041  dfdm2  5043  funimaexg  5177  dfmpt3  5215  mptun  5224  funcocnv2  5360  fnasrn  5566  fnasrng  5568  fpr  5570  fmptap  5578  riotav  5703  dmoprab  5820  rnoprab2  5823  mpov  5829  mpomptx  5830  abrexex2g  5986  abrexex2  5990  1stval2  6021  2ndval2  6022  fo1st  6023  fo2nd  6024  xp2  6039  dfoprab4f  6059  fmpoco  6081  tposmpo  6146  recsfval  6180  frecfnom  6266  freccllem  6267  frecfcllem  6269  frecsuclem  6271  df2o3  6295  o1p1e2  6332  ecqs  6459  qliftf  6482  erovlem  6489  mapsnf1o3  6559  ixp0x  6588  xpf1o  6706  djuunr  6919  dmaddpq  7155  dmmulpq  7156  enq0enq  7207  nqprlu  7323  m1p1sr  7536  m1m1sr  7537  caucvgsr  7578  dfcnqs  7617  3m1e2  8808  2p2e4  8815  3p2e5  8829  3p3e6  8830  4p2e6  8831  4p3e7  8832  4p4e8  8833  5p2e7  8834  5p3e8  8835  5p4e9  8836  6p2e8  8837  6p3e9  8838  7p2e9  8839  nn0supp  8997  nnzrab  9046  nn0zrab  9047  dec0u  9170  dec0h  9171  decsuc  9180  decsucc  9190  numma  9193  decma  9200  decmac  9201  decma2c  9202  decadd  9203  decaddc  9204  decmul1  9213  decmul1c  9214  decmul2c  9215  5p5e10  9220  6p4e10  9221  7p3e10  9224  8p2e10  9229  5t5e25  9252  6t6e36  9257  8t6e48  9268  nn0uz  9328  nnuz  9329  xaddcom  9612  ioomax  9699  iccmax  9700  ioopos  9701  ioorp  9702  fseq1p1m1  9842  fzo0to2pr  9963  fzo0to3tp  9964  frecfzennn  10167  irec  10360  sq10e99m1  10428  facnn  10441  fac0  10442  faclbnd2  10456  zfz1isolemsplit  10549  minmax  10969  xrminmax  11002  fisumrev2  11183  fsumparts  11207  fsumiun  11214  isumnn0nn  11230  ege2le3  11304  cos1bnd  11393  efieq1re  11405  eirraplem  11410  phiprmpw  11825  unennn  11837  ennnfonelemjn  11842  qnnen  11871  strle1g  11976  tgrest  12265  uniretop  12621  dvexp  12771  dvef  12783  cospi  12808  sincos6thpi  12850  bj-omind  13059
  Copyright terms: Public domain W3C validator