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

Theorem eqtr2i 2199
Description: An equality transitivity inference. (Contributed by NM, 21-Feb-1995.)
Hypotheses
Ref Expression
eqtr2i.1  |-  A  =  B
eqtr2i.2  |-  B  =  C
Assertion
Ref Expression
eqtr2i  |-  C  =  A

Proof of Theorem eqtr2i
StepHypRef Expression
1 eqtr2i.1 . . 3  |-  A  =  B
2 eqtr2i.2 . . 3  |-  B  =  C
31, 2eqtri 2198 . 2  |-  A  =  C
43eqcomi 2181 1  |-  C  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1353
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-cleq 2170
This theorem is referenced by:  3eqtrri  2203  3eqtr2ri  2205  symdif1  3402  dfif3  3549  dfsn2  3608  prprc1  3702  ruv  4551  xpindi  4764  xpindir  4765  dmcnvcnv  4853  rncnvcnv  4854  imainrect  5076  dfrn4  5091  fcoi1  5398  foimacnv  5481  fsnunfv  5719  dfoprab3  6194  fiintim  6930  sbthlemi8  6965  pitonnlem1  7846  ixi  8542  recexaplem2  8611  zeo  9360  num0h  9397  dec10p  9428  fseq1p1m1  10096  fsumrelem  11481  ef0lem  11670  ef01bndlem  11766  3lcm2e6woprm  12088  strsl0  12513  0g0  12800  tgioo  14085  tgqioo  14086  dveflem  14226  sincos4thpi  14300  coskpi  14308
  Copyright terms: Public domain W3C validator