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

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

Proof of Theorem syl5eq
StepHypRef Expression
1 syl5eq.1 . . 3  |-  A  =  B
21a1i 9 . 2  |-  ( ph  ->  A  =  B )
3 syl5eq.2 . 2  |-  ( ph  ->  B  =  C )
42, 3eqtrd 2150 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:  syl5req  2163  syl5eqr  2164  3eqtr3a  2174  3eqtr4g  2175  csbtt  2985  csbvarg  3000  csbie2g  3020  rabbi2dva  3254  csbprc  3378  disjssun  3396  disjpr2  3557  prprc2  3602  difprsn2  3630  opprc  3696  intsng  3775  riinm  3855  iinxsng  3856  iunxprg  3863  rintm  3875  sucprc  4304  unisucg  4306  xpriindim  4647  relop  4659  dmxpm  4729  riinint  4770  resabs1  4818  resabs2  4820  resima2  4823  xpssres  4824  resopab2  4836  imasng  4874  ndmima  4886  xpdisj1  4933  xpdisj2  4934  djudisj  4936  resdisj  4937  rnxpm  4938  xpima1  4955  xpima2m  4956  dmsnsnsng  4986  rnsnopg  4987  rnpropg  4988  mptiniseg  5003  dfco2a  5009  relcoi1  5040  unixpm  5044  iotaval  5069  funtp  5146  fnun  5199  fnresdisj  5203  fnima  5211  fnimaeq0  5214  fcoi1  5273  f1orescnv  5351  foun  5354  resdif  5357  tz6.12-2  5380  fveu  5381  tz6.12-1  5416  fvun2  5456  fvopab3ig  5463  f1oresrab  5553  dfmptg  5567  ressnop0  5569  fvunsng  5582  fnsnsplitss  5587  fsnunfv  5589  fvpr1  5592  fvpr2  5593  fvpr1g  5594  fvpr2g  5595  fvtp1g  5596  fvtp2g  5597  fvtp3g  5598  fvtp2  5600  fvtp3  5601  f1oiso2  5696  riotaund  5732  ovprc  5774  resoprab2  5836  fnoprabg  5840  ovidig  5856  ovigg  5859  ov6g  5876  ovconst2  5890  offval2  5965  ot1stg  6018  ot2ndg  6019  ot3rdgg  6020  fmpoco  6081  algrflemg  6095  tpostpos2  6130  rdgisuc1  6249  frec0g  6262  frecsuclem  6271  frecrdg  6273  oasuc  6328  oa1suc  6331  omsuc  6336  nnm1  6388  nnm2  6389  dfec2  6400  errn  6419  ixpsnval  6563  ixpintm  6587  mapen  6708  xpmapenlem  6711  phplem2  6715  undifdc  6780  fisseneq  6788  ssfirab  6790  eqinfti  6875  infvalti  6877  infsnti  6885  casef  6941  caseinl  6944  caseinr  6945  djudom  6946  ctssdccl  6964  exmidfodomrlemim  7025  1qec  7164  mulidnq  7165  addpinq1  7240  suplocexprlem2b  7490  suplocexprlemlub  7500  0idsr  7543  1idsr  7544  caucvgsrlemoffres  7576  caucvgsr  7578  mulresr  7614  pitonnlem2  7623  ax1rid  7653  axcnre  7657  negid  7977  subneg  7979  negneg  7980  dfinfre  8678  2times  8806  infrenegsupex  9345  rexneg  9568  xaddpnf2  9585  xaddmnf1  9586  xaddmnf2  9587  fseq1p1m1  9829  fzosplitprm1  9966  intfracq  10048  frec2uz0d  10127  frec2uzrdg  10137  frecuzrdg0  10141  frecuzrdgg  10144  frecuzrdg0t  10150  seq3val  10186  seqvalcd  10187  iseqf1olemjpcl  10223  iseqf1olemqpcl  10224  iseqf1olemfvp  10225  seq3f1olemqsum  10228  sqval  10306  iexpcyc  10352  binom3  10364  faclbnd  10442  faclbnd2  10443  bcn1  10459  hashinfom  10479  hashennn  10481  hashxp  10527  shftlem  10543  shftuz  10544  shftidt  10560  reim0  10588  remullem  10598  resqrexlemf1  10735  resqrexlemcalc3  10743  absexpzap  10807  absimle  10811  amgm2  10845  minmax  10956  xrmaxiflemval  10974  xrmaxadd  10985  infxrnegsupex  10987  xrminmax  10989  summodc  11107  fsum3  11111  sumsnf  11133  sumsns  11139  isumclim3  11147  isumge0  11154  fsump1i  11157  fsum2dlemstep  11158  fisumcom2  11162  fsumshftm  11169  fsumconst  11178  fsumiun  11201  hashrabrex  11205  hashuni  11206  binom11  11210  isumsplit  11215  geo2sum  11238  mertensabs  11261  efgt1p2  11315  efgt1p  11316  resinval  11336  recosval  11337  cosadd  11358  ef01bndlem  11377  eirraplem  11395  ialgr0  11637  algrp1  11639  eucalg  11652  phiprmpw  11809  phiprm  11810  ennnfonelem0  11829  ennnfonelemfun  11841  ennnfonelemf1  11842  ennnfonelemrn  11843  ctinfomlemom  11851  ndxid  11894  setsfun0  11906  setsresg  11908  setscom  11910  strslfv2d  11912  ressid2  11929  ressval2  11930  tgidm  12154  tgrest  12249  ssidcn  12290  txcnmpt  12353  txcn  12355  blres  12514  mopnval  12522  remetdval  12619  divccncfap  12657  cncfmet  12659  cncfcncntop  12660  cnplimcim  12716  cnplimclemr  12718  limccnpcntop  12724  limccnp2cntop  12726  dvexp  12755  sin0pilem1  12773  pilem3  12775  ef2kpi  12798  sin2pim  12805  cos2pim  12806  sinmpi  12807  cosmpi  12808  sinppi  12809  cosppi  12810  sinhalfpip  12812  sinhalfpim  12813  coshalfpip  12814  coshalfpim  12815  ex-ceil  12834  qdencn  13118  cvgcmp2nlemabs  13123  trilpolemlt1  13130
  Copyright terms: Public domain W3C validator