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

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

Proof of Theorem syl6reqr
StepHypRef Expression
1 syl6reqr.1 . 2
2 syl6reqr.2 . . 3
32eqcomi 2143 . 2
41, 3syl6req 2189 1
 Colors of variables: wff set class Syntax hints:   wi 4   wceq 1331 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2121 This theorem depends on definitions:  df-bi 116  df-cleq 2132 This theorem is referenced by:  iftrue  3479  iffalse  3482  difprsn1  3659  dmmptg  5036  relcoi1  5070  funimacnv  5199  dmmptd  5253  dffv3g  5417  dfimafn  5470  fvco2  5490  isoini  5719  oprabco  6114  ixpconstg  6601  unfiexmid  6806  undifdc  6812  sbthlemi4  6848  sbthlemi5  6849  sbthlemi6  6850  supval2ti  6882  exmidfodomrlemim  7057  suplocexprlemex  7530  eqneg  8492  zeo  9156  fseq1p1m1  9874  seq3val  10231  seqvalcd  10232  hashfzo  10568  hashxp  10572  fsumconst  11223  modfsummod  11227  telfsumo  11235  mulgcd  11704  algcvg  11729  phiprmpw  11898  strslfv3  12004  uptx  12443  resubmet  12717
 Copyright terms: Public domain W3C validator