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

Theorem syl5eqr 2399
 Description: An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl5eqr.1
syl5eqr.2
Assertion
Ref Expression
syl5eqr

Proof of Theorem syl5eqr
StepHypRef Expression
1 syl5eqr.1 . . 3
21eqcomi 2357 . 2
3 syl5eqr.2 . 2
42, 3syl5eq 2397 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:  3eqtr3g  2408  csbeq1a  3144  ssdifeq0  3632  pw1equn  4331  sfinltfin  4535  vfintle  4546  phialllem2  4617  opabbi2dv  4867  fcoi1  5240  f1imacnv  5302  foimacnv  5303  f1ococnv1  5310  funfv  5375  fsn2  5434  funiunfvf  5468  f1ocnvfv2  5477  brcomposeg  5819  mapsn  6026  enpw1  6062  enmap2  6068  enmap1lem5  6073  ncdisjun  6136
 Copyright terms: Public domain W3C validator