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

Theorem syl6reqr 2088
Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
Hypotheses
Ref Expression
syl6reqr.1
syl6reqr.2  C
Assertion
Ref Expression
syl6reqr  C

Proof of Theorem syl6reqr
StepHypRef Expression
1 syl6reqr.1 . 2
2 syl6reqr.2 . . 3  C
32eqcomi 2041 . 2  C
41, 3syl6req 2086 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:  iftrue  3330  iffalse  3333  difprsn1  3494  dmmptg  4761  relcoi1  4792  funimacnv  4918  dffv3g  5117  dfimafn  5165  fvco2  5185  isoini  5400  oprabco  5780  eqneg  7490  zeo  8119  fseq1p1m1  8726  iseqval  8900
  Copyright terms: Public domain W3C validator