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

Theorem eqtr2i 2179
 Description: An equality transitivity inference. (Contributed by NM, 21-Feb-1995.)
Hypotheses
Ref Expression
eqtr2i.1
eqtr2i.2
Assertion
Ref Expression
eqtr2i

Proof of Theorem eqtr2i
StepHypRef Expression
1 eqtr2i.1 . . 3
2 eqtr2i.2 . . 3
31, 2eqtri 2178 . 2
43eqcomi 2161 1
 Colors of variables: wff set class Syntax hints:   wceq 1335 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 1427  ax-gen 1429  ax-4 1490  ax-17 1506  ax-ext 2139 This theorem depends on definitions:  df-bi 116  df-cleq 2150 This theorem is referenced by:  3eqtrri  2183  3eqtr2ri  2185  symdif1  3372  dfif3  3518  dfsn2  3574  prprc1  3667  ruv  4508  xpindi  4720  xpindir  4721  dmcnvcnv  4809  rncnvcnv  4810  imainrect  5030  dfrn4  5045  fcoi1  5349  foimacnv  5431  fsnunfv  5667  dfoprab3  6136  fiintim  6870  sbthlemi8  6905  pitonnlem1  7759  ixi  8452  recexaplem2  8520  zeo  9263  num0h  9300  dec10p  9331  fseq1p1m1  9989  fsumrelem  11361  ef0lem  11550  ef01bndlem  11646  3lcm2e6woprm  11954  strsl0  12209  tgioo  12917  tgqioo  12918  dveflem  13058  sincos4thpi  13132  coskpi  13140
 Copyright terms: Public domain W3C validator