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

Theorem syl5eq 2100
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 2088 1  |-  ( ph  ->  A  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1259
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-4 1416  ax-17 1435  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-cleq 2049
This theorem is referenced by:  syl5req  2101  syl5eqr  2102  3eqtr3a  2112  3eqtr4g  2113  csbtt  2890  csbvarg  2905  csbie2g  2924  rabbi2dva  3173  csbprc  3290  disjssun  3313  disjpr2  3462  prprc2  3507  difprsn2  3532  opprc  3598  intsng  3677  riinm  3757  iinxsng  3758  rintm  3772  sucprc  4177  unisucg  4179  xpriindim  4502  relop  4514  dmxpm  4583  riinint  4621  resabs1  4668  resabs2  4669  resima2  4672  xpssres  4673  resopab2  4683  imasng  4718  ndmima  4730  xpdisj1  4775  xpdisj2  4776  djudisj  4778  resdisj  4779  rnxpm  4780  xpima1  4795  xpima2m  4796  dmsnsnsng  4826  rnsnopg  4827  rnpropg  4828  mptiniseg  4843  dfco2a  4849  relcoi1  4877  unixpm  4881  iotaval  4906  funtp  4980  fnun  5033  fnresdisj  5037  fnima  5045  fnimaeq0  5048  fcoi1  5098  f1orescnv  5170  foun  5173  resdif  5176  tz6.12-2  5197  fveu  5198  tz6.12-1  5228  fvun2  5268  fvopab3ig  5274  f1oresrab  5357  dfmptg  5370  ressnop0  5372  fvunsng  5385  fsnunfv  5391  fvpr1  5393  fvpr2  5394  fvpr1g  5395  fvpr2g  5396  fvtp1g  5397  fvtp2g  5398  fvtp3g  5399  fvtp2  5401  fvtp3  5402  f1oiso2  5494  riotaund  5530  ovprc  5568  resoprab2  5626  fnoprabg  5630  ovidig  5646  ovigg  5649  ov6g  5666  ovconst2  5680  offval2  5754  ot1stg  5807  ot2ndg  5808  ot3rdgg  5809  fmpt2co  5865  algrflemg  5879  tpostpos2  5911  rdgisuc1  6002  frec0g  6014  frecsuclem1  6018  frecsuclem2  6020  frecrdg  6023  oasuc  6075  oa1suc  6078  omsuc  6082  nnm1  6128  nnm2  6129  dfec2  6140  errn  6159  phplem2  6347  1qec  6544  mulidnq  6545  addpinq1  6620  0idsr  6910  1idsr  6911  caucvgsrlemoffres  6942  caucvgsr  6944  mulresr  6972  pitonnlem2  6981  ax1rid  7009  axcnre  7013  negid  7321  subneg  7323  negneg  7324  2times  8111  rexneg  8844  fseq1p1m1  9058  fzosplitprm1  9192  intfracq  9270  frec2uz0d  9349  frec2uzrdg  9359  frecuzrdg0  9364  iseqval  9384  sqval  9478  iexpcyc  9523  binom3  9534  faclbnd  9609  faclbnd2  9610  bcn1  9626  shftlem  9645  shftuz  9646  shftidt  9662  reim0  9689  remullem  9699  resqrexlemf1  9835  resqrexlemcalc3  9843  absexpzap  9907  absimle  9911  amgm2  9945  ialgr0  10266  ialgrp1  10268  ex-ceil  10280  qdencn  10511
  Copyright terms: Public domain W3C validator