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

Theorem sylan9eq 2405
Description: An equality transitivity deduction. (Contributed by NM, 8-May-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypotheses
Ref Expression
sylan9eq.1
sylan9eq.2
Assertion
Ref Expression
sylan9eq

Proof of Theorem sylan9eq
StepHypRef Expression
1 sylan9eq.1 . 2
2 sylan9eq.2 . 2
3 eqtr 2370 . 2
41, 2, 3syl2an 463 1
Colors of variables: wff setvar class
Syntax hints:   wi 4   wa 358   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-an 360  df-ex 1542  df-cleq 2346
This theorem is referenced by:  sylan9req  2406  sylan9eqr  2407  nineq12  3236  symdifeq12  3250  difeq12  3380  uneq12  3413  ineq12  3452  ifeq12  3675  ifbi  3679  preq12  3801  opkeq12  4061  preq12b  4127  xpkeq12  4200  addceq12  4385  opeq12  4580  xpeq12  4803  nfimad  4954  funimass1  5169  f1orescnv  5301  resdif  5306  oveq12  5532  caovmo  5645  cbvmpt2v  5680  fvmpt2  5704  ovmpt2g  5715  fvmptnf  5723  map0  6025  enmap2lem5  6067  enmap1lem3  6071  enmap1lem5  6073
  Copyright terms: Public domain W3C validator