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

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

Proof of Theorem syl5eqr
StepHypRef Expression
1 syl5eqr.1 . . 3
21eqcomi 2041 . 2
3 syl5eqr.2 . 2  C
42, 3syl5eq 2081 1  C
Colors of variables: wff set class
Syntax hints:   wi 4   wceq 1242
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-gen 1335  ax-4 1397  ax-17 1416  ax-ext 2019
This theorem depends on definitions:  df-bi 110  df-cleq 2030
This theorem is referenced by:  3eqtr3g  2092  csbeq1a  2854  ssdifeq0  3299  pofun  4040  opabbi2dv  4428  funimaexg  4926  fresin  5011  f1imacnv  5086  foimacnv  5087  fsn2  5280  fmptpr  5298  funiunfvdm  5345  funiunfvdmf  5346  fcof1o  5372  f1opw2  5648  fnexALT  5682  eqerlem  6073  fopwdom  6246  mul02  7160  recdivap  7456  fzpreddisj  8683  fzshftral  8720  frec2uzrdg  8856  binom3  8999  cnrecnv  9118
  Copyright terms: Public domain W3C validator