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

Theorem syl5eqr 2186
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 2143 . 2  |-  A  =  B
3 syl5eqr.2 . 2  |-  ( ph  ->  B  =  C )
42, 3syl5eq 2184 1  |-  ( ph  ->  A  =  C )
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:  3eqtr3g  2195  csbeq1a  3012  ssdifeq0  3445  pofun  4234  opabbi2dv  4688  funimaexg  5207  fresin  5301  f1imacnv  5384  foimacnv  5385  fsn2  5594  fmptpr  5612  funiunfvdm  5664  funiunfvdmf  5665  fcof1o  5690  f1opw2  5976  fnexALT  6011  eqerlem  6460  pmresg  6570  mapsn  6584  fopwdom  6730  mapen  6740  fiintim  6817  xpfi  6818  sbthlemi8  6852  sbthlemi9  6853  ctssdccl  6996  exmidfodomrlemim  7057  mul02  8156  recdivap  8485  fzpreddisj  9858  fzshftral  9895  qbtwnrelemcalc  10040  frec2uzrdg  10189  frecuzrdgrcl  10190  frecuzrdgsuc  10194  frecuzrdgrclt  10195  frecuzrdgg  10196  binom3  10416  bcn2  10517  hashfz1  10536  hashunlem  10557  hashfacen  10586  cnrecnv  10689  resqrexlemnm  10797  amgm2  10897  2zsupmax  11004  xrmaxltsup  11034  xrmaxadd  11037  xrbdtri  11052  fisumss  11168  fsumcnv  11213  telfsumo  11242  fsumiun  11253  arisum2  11275  ege2le3  11384  efgt1p  11409  cos01bnd  11471  dfgcd3  11704  eucalgval  11741  sqrt2irrlem  11845  setsslid  12018  baspartn  12226  txdis1cn  12456  cnmpt21  12469  cnmpt22  12472  hmeores  12493  metreslem  12558  remetdval  12717  dvfvalap  12828  nninfsellemqall  13264
  Copyright terms: Public domain W3C validator