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

Theorem eqtr4i 2045
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 2026 . 2 B = 𝐶
41, 3eqtri 2042 1 A = 𝐶
Colors of variables: wff set class
Syntax hints:   = wceq 1228
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 1316  ax-gen 1318  ax-4 1381  ax-17 1400  ax-ext 2004
This theorem depends on definitions:  df-bi 110  df-cleq 2015
This theorem is referenced by:  3eqtr2i  2048  3eqtr2ri  2049  3eqtr4i  2052  3eqtr4ri  2053  rabab  2552  cbvralcsf  2885  cbvrexcsf  2886  cbvrabcsf  2888  dfin5  2902  dfdif2  2903  uneqin  3165  unrab  3185  inrab  3186  inrab2  3187  difrab  3188  dfrab3ss  3192  rabun2  3193  difidALT  3270  difdifdirss  3284  dfif3  3320  tpidm  3446  dfint2  3591  iunrab  3678  uniiun  3684  intiin  3685  0iin  3689  mptv  3827  xpundi  4323  xpundir  4324  resiun2  4558  resopab  4579  opabresid  4586  dfse2  4625  cnvun  4656  cnvin  4658  imaundir  4664  imainrect  4693  cnvcnv2  4701  cnvcnvres  4711  dmtpop  4723  rnsnopg  4726  rnco2  4755  dmco  4756  co01  4762  unidmrn  4777  dfdm2  4779  funimaexg  4909  dfmpt3  4947  mptun  4955  funcocnv2  5076  fnasrn  5266  fnasrng  5268  fpr  5270  fmptap  5278  riotav  5397  dmoprab  5508  rnoprab2  5511  mpt2v  5517  mpt2mptx  5518  abrexex2g  5670  abrexex2  5674  1stval2  5705  2ndval2  5706  fo1st  5707  fo2nd  5708  xp2  5722  dfoprab4f  5742  fmpt2co  5760  tposmpt2  5818  recsfval  5853  frecfnom  5901  frecsuclem1  5903  frecsuclem2  5905  df2o3  5929  o1p1e2  5963  ecqs  6079  qliftf  6102  erovlem  6109  dmaddpq  6238  dmmulpq  6239  enq0enq  6286  m1p1sr  6507  m1m1sr  6508  dfcnqs  6552  bj-omind  7156
  Copyright terms: Public domain W3C validator