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

Theorem eqtr4i 2163
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 2143 . 2 𝐵 = 𝐶
41, 3eqtri 2160 1 𝐴 = 𝐶
Colors of variables: wff set class
Syntax hints:   = wceq 1331
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 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2121
This theorem depends on definitions:  df-bi 116  df-cleq 2132
This theorem is referenced by:  3eqtr2i  2166  3eqtr2ri  2167  3eqtr4i  2170  3eqtr4ri  2171  rabab  2707  cbvralcsf  3062  cbvrexcsf  3063  cbvrabcsf  3065  dfin5  3078  dfdif2  3079  uneqin  3327  unrab  3347  inrab  3348  inrab2  3349  difrab  3350  dfrab3ss  3354  rabun2  3355  difidALT  3432  difdifdirss  3447  dfif3  3487  tpidm  3625  dfint2  3773  iunrab  3860  uniiun  3866  intiin  3867  0iin  3871  mptv  4025  xpundi  4595  xpundir  4596  resiun2  4839  resopab  4863  opabresid  4872  dfse2  4912  cnvun  4944  cnvin  4946  imaundir  4952  imainrect  4984  cnvcnv2  4992  cnvcnvres  5002  dmtpop  5014  rnsnopg  5017  rnco2  5046  dmco  5047  co01  5053  unidmrn  5071  dfdm2  5073  funimaexg  5207  dfmpt3  5245  mptun  5254  funcocnv2  5392  fnasrn  5598  fnasrng  5600  fpr  5602  fmptap  5610  riotav  5735  dmoprab  5852  rnoprab2  5855  mpov  5861  mpomptx  5862  abrexex2g  6018  abrexex2  6022  1stval2  6053  2ndval2  6054  fo1st  6055  fo2nd  6056  xp2  6071  dfoprab4f  6091  fmpoco  6113  tposmpo  6178  recsfval  6212  frecfnom  6298  freccllem  6299  frecfcllem  6301  frecsuclem  6303  df2o3  6327  o1p1e2  6364  ecqs  6491  qliftf  6514  erovlem  6521  mapsnf1o3  6591  ixp0x  6620  xpf1o  6738  djuunr  6951  dmaddpq  7201  dmmulpq  7202  enq0enq  7253  nqprlu  7369  m1p1sr  7582  m1m1sr  7583  caucvgsr  7624  dfcnqs  7663  3m1e2  8854  2p2e4  8861  3p2e5  8875  3p3e6  8876  4p2e6  8877  4p3e7  8878  4p4e8  8879  5p2e7  8880  5p3e8  8881  5p4e9  8882  6p2e8  8883  6p3e9  8884  7p2e9  8885  nn0supp  9043  nnzrab  9092  nn0zrab  9093  dec0u  9216  dec0h  9217  decsuc  9226  decsucc  9236  numma  9239  decma  9246  decmac  9247  decma2c  9248  decadd  9249  decaddc  9250  decmul1  9259  decmul1c  9260  decmul2c  9261  5p5e10  9266  6p4e10  9267  7p3e10  9270  8p2e10  9275  5t5e25  9298  6t6e36  9303  8t6e48  9314  nn0uz  9374  nnuz  9375  xaddcom  9658  ioomax  9745  iccmax  9746  ioopos  9747  ioorp  9748  fseq1p1m1  9888  fzo0to2pr  10009  fzo0to3tp  10010  frecfzennn  10213  irec  10406  sq10e99m1  10474  facnn  10487  fac0  10488  faclbnd2  10502  zfz1isolemsplit  10595  minmax  11015  xrminmax  11048  fisumrev2  11229  fsumparts  11253  fsumiun  11260  isumnn0nn  11276  ege2le3  11391  cos1bnd  11479  efieq1re  11491  eirraplem  11496  phiprmpw  11911  unennn  11923  ennnfonelemjn  11928  qnnen  11957  strle1g  12065  tgrest  12354  uniretop  12710  dvexp  12860  dvef  12873  cospi  12905  sincos6thpi  12947  bj-omind  13239
  Copyright terms: Public domain W3C validator