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

Theorem syl5reqr 2163
Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
Hypotheses
Ref Expression
syl5reqr.1  |-  B  =  A
syl5reqr.2  |-  ( ph  ->  B  =  C )
Assertion
Ref Expression
syl5reqr  |-  ( ph  ->  C  =  A )

Proof of Theorem syl5reqr
StepHypRef Expression
1 syl5reqr.1 . . 3  |-  B  =  A
21eqcomi 2119 . 2  |-  A  =  B
3 syl5reqr.2 . 2  |-  ( ph  ->  B  =  C )
42, 3syl5req 2161 1  |-  ( ph  ->  C  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1314
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 1406  ax-gen 1408  ax-4 1470  ax-17 1489  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-cleq 2108
This theorem is referenced by:  bm2.5ii  4380  resdmdfsn  4830  f0dom0  5284  f1o00  5368  fmpt  5536  fmptsn  5575  resfunexg  5607  mapsn  6550  sbthlemi4  6814  sbthlemi6  6816  pm54.43  7012  prarloclem5  7272  recexprlem1ssl  7405  recexprlem1ssu  7406  iooval2  9638  hashsng  10484  zfz1isolem1  10523  resqrexlemover  10722  isumclim3  11132  algrp1  11623  subctctexmid  12998
  Copyright terms: Public domain W3C validator