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

Theorem syl5eqr 2128
Description: An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl5eqr.1  |-  B  =  A
syl5eqr.2  |-  ( ph  ->  B  =  C )
Assertion
Ref Expression
syl5eqr  |-  ( ph  ->  A  =  C )

Proof of Theorem syl5eqr
StepHypRef Expression
1 syl5eqr.1 . . 3  |-  B  =  A
21eqcomi 2086 . 2  |-  A  =  B
3 syl5eqr.2 . 2  |-  ( ph  ->  B  =  C )
42, 3syl5eq 2126 1  |-  ( ph  ->  A  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1285
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-4 1441  ax-17 1460  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-cleq 2075
This theorem is referenced by:  3eqtr3g  2137  csbeq1a  2917  ssdifeq0  3332  pofun  4075  opabbi2dv  4513  funimaexg  5014  fresin  5099  f1imacnv  5174  foimacnv  5175  fsn2  5369  fmptpr  5387  funiunfvdm  5434  funiunfvdmf  5435  fcof1o  5460  f1opw2  5737  fnexALT  5771  eqerlem  6203  fopwdom  6380  mul02  7558  recdivap  7873  fzpreddisj  9164  fzshftral  9201  qbtwnrelemcalc  9342  frec2uzrdg  9491  frecuzrdgrcl  9492  frecuzrdgsuc  9496  frecuzrdgrclt  9497  frecuzrdgg  9498  binom3  9687  bcn2  9788  sizefz1  9807  sizeunlem  9828  cnrecnv  9935  resqrexlemnm  10042  amgm2  10142  dfgcd3  10543  eucalgval  10580  sqrt2irrlem  10684
  Copyright terms: Public domain W3C validator