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

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

Proof of Theorem syl6eqr
StepHypRef Expression
1 syl6eqr.1 . 2
2 syl6eqr.2 . . 3  C
32eqcomi 2041 . 2  C
41, 3syl6eq 2085 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:  3eqtr4g  2094  rabxmdc  3243  relop  4429  csbcnvg  4462  dfiun3g  4532  dfiin3g  4533  resima2  4587  relcnvfld  4794  uniabio  4820  fntpg  4898  dffn5im  5162  dfimafn2  5166  fncnvima2  5231  fmptcof  5274  fcoconst  5277  fnasrng  5286  ffnov  5547  fnovim  5551  fnrnov  5588  foov  5589  funimassov  5592  ovelimab  5593  ofc12  5673  caofinvl  5675  dftpos3  5818  tfr0  5878  rdgisucinc  5912  oasuc  5983  ecinxp  6117  indpi  6326  nqnq0pi  6421  nq0m0r  6439  addnqpr1  6543  recexgt0sr  6701  axrnegex  6763  cnref1o  8357  fztp  8710  fseq1m1p1  8727  frecuzrdgrrn  8875  frecuzrdgsuc  8882  mulexpzap  8949  expaddzap  8953  cjexp  9121
  Copyright terms: Public domain W3C validator