New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  3eqtr4a Unicode version

Theorem 3eqtr4a 2411
 Description: A chained equality inference, useful for converting to definitions. (Contributed by NM, 2-Feb-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypotheses
Ref Expression
3eqtr4a.1
3eqtr4a.2
3eqtr4a.3
Assertion
Ref Expression
3eqtr4a

Proof of Theorem 3eqtr4a
StepHypRef Expression
1 3eqtr4a.2 . . 3
2 3eqtr4a.1 . . 3
31, 2syl6eq 2401 . 2
4 3eqtr4a.3 . 2
53, 4eqtr4d 2388 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wceq 1642 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746  ax-ext 2334 This theorem depends on definitions:  df-bi 177  df-ex 1542  df-cleq 2346 This theorem is referenced by:  uniintsn  3963  iununi  4050  pw1eqadj  4332  tfincl  4492  dmxpid  4924  imasn  5018  rnxpid  5054  1st2nd2  5516  uniqs2  5985  muccom  6134  mucass  6135  mucid1  6143  tcdi  6164  tce2  6236  nchoicelem2  6290
 Copyright terms: Public domain W3C validator