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

Theorem syl5eqr 2164
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 2121 . 2  |-  A  =  B
3 syl5eqr.2 . 2  |-  ( ph  ->  B  =  C )
42, 3syl5eq 2162 1  |-  ( ph  ->  A  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1316
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 1408  ax-gen 1410  ax-4 1472  ax-17 1491  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-cleq 2110
This theorem is referenced by:  3eqtr3g  2173  csbeq1a  2983  ssdifeq0  3415  pofun  4204  opabbi2dv  4658  funimaexg  5177  fresin  5271  f1imacnv  5352  foimacnv  5353  fsn2  5562  fmptpr  5580  funiunfvdm  5632  funiunfvdmf  5633  fcof1o  5658  f1opw2  5944  fnexALT  5979  eqerlem  6428  pmresg  6538  mapsn  6552  fopwdom  6698  mapen  6708  fiintim  6785  xpfi  6786  sbthlemi8  6820  sbthlemi9  6821  ctssdccl  6964  exmidfodomrlemim  7025  mul02  8117  recdivap  8446  fzpreddisj  9819  fzshftral  9856  qbtwnrelemcalc  10001  frec2uzrdg  10150  frecuzrdgrcl  10151  frecuzrdgsuc  10155  frecuzrdgrclt  10156  frecuzrdgg  10157  binom3  10377  bcn2  10478  hashfz1  10497  hashunlem  10518  hashfacen  10547  cnrecnv  10650  resqrexlemnm  10758  amgm2  10858  2zsupmax  10965  xrmaxltsup  10995  xrmaxadd  10998  xrbdtri  11013  fisumss  11129  fsumcnv  11174  telfsumo  11203  fsumiun  11214  arisum2  11236  ege2le3  11304  efgt1p  11329  cos01bnd  11392  dfgcd3  11625  eucalgval  11662  sqrt2irrlem  11766  setsslid  11936  baspartn  12144  txdis1cn  12374  cnmpt21  12387  cnmpt22  12390  hmeores  12411  metreslem  12476  remetdval  12635  dvfvalap  12746  nninfsellemqall  13138
  Copyright terms: Public domain W3C validator