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

Theorem 3eqtr4ri 2384
 Description: An inference from three chained equalities. (Contributed by NM, 2-Sep-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypotheses
Ref Expression
3eqtr4i.1
3eqtr4i.2
3eqtr4i.3
Assertion
Ref Expression
3eqtr4ri

Proof of Theorem 3eqtr4ri
StepHypRef Expression
1 3eqtr4i.3 . . 3
2 3eqtr4i.1 . . 3
31, 2eqtr4i 2376 . 2
4 3eqtr4i.2 . 2
53, 4eqtr4i 2376 1
 Colors of variables: wff setvar class Syntax hints:   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:  cbvreucsf  3200  dfin3  3494  dfin5  3545  dfif6  3665  qdass  3819  tpidm12  3821  ssfin  4470  nnadjoin  4520  nulnnn  4556  df1st2  4738  dfsset2  4743  dfco1  4748  dfsi2  4751  resres  4980  inres  4985  cnvun  5033  coundi  5082  coundir  5083  snec  5987  df0c2  6137  1cnc  6139  1p1e2c  6155  2p1e3c  6156
 Copyright terms: Public domain W3C validator