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

Theorem syl5eq 2129
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 2117 1  |-  ( ph  ->  A  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1287
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 1379  ax-gen 1381  ax-4 1443  ax-17 1462  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-cleq 2078
This theorem is referenced by:  syl5req  2130  syl5eqr  2131  3eqtr3a  2141  3eqtr4g  2142  csbtt  2932  csbvarg  2947  csbie2g  2967  rabbi2dva  3197  csbprc  3316  disjssun  3334  disjpr2  3489  prprc2  3534  difprsn2  3560  opprc  3626  intsng  3705  riinm  3785  iinxsng  3786  rintm  3800  sucprc  4213  unisucg  4215  xpriindim  4542  relop  4554  dmxpm  4624  riinint  4662  resabs1  4709  resabs2  4710  resima2  4713  xpssres  4714  resopab2  4726  imasng  4764  ndmima  4776  xpdisj1  4821  xpdisj2  4822  djudisj  4824  resdisj  4825  rnxpm  4826  xpima1  4843  xpima2m  4844  dmsnsnsng  4874  rnsnopg  4875  rnpropg  4876  mptiniseg  4891  dfco2a  4897  relcoi1  4928  unixpm  4932  iotaval  4957  funtp  5032  fnun  5085  fnresdisj  5089  fnima  5097  fnimaeq0  5100  fcoi1  5154  f1orescnv  5232  foun  5235  resdif  5238  tz6.12-2  5259  fveu  5260  tz6.12-1  5294  fvun2  5334  fvopab3ig  5341  f1oresrab  5426  dfmptg  5439  ressnop0  5441  fvunsng  5454  fsnunfv  5460  fvpr1  5462  fvpr2  5463  fvpr1g  5464  fvpr2g  5465  fvtp1g  5466  fvtp2g  5467  fvtp3g  5468  fvtp2  5470  fvtp3  5471  f1oiso2  5567  riotaund  5603  ovprc  5641  resoprab2  5699  fnoprabg  5703  ovidig  5719  ovigg  5722  ov6g  5739  ovconst2  5753  offval2  5827  ot1stg  5880  ot2ndg  5881  ot3rdgg  5882  fmpt2co  5938  algrflemg  5952  tpostpos2  5984  rdgisuc1  6103  frec0g  6116  frecsuclem  6125  frecrdg  6127  oasuc  6179  oa1suc  6182  omsuc  6187  nnm1  6235  nnm2  6236  dfec2  6247  errn  6266  mapen  6514  xpmapenlem  6517  phplem2  6521  undifdc  6586  fisseneq  6592  ssfirab  6593  eqinfti  6659  infvalti  6661  infsnti  6669  casef  6723  djudom  6731  exmidfodomrlemim  6771  1qec  6891  mulidnq  6892  addpinq1  6967  0idsr  7257  1idsr  7258  caucvgsrlemoffres  7289  caucvgsr  7291  mulresr  7319  pitonnlem2  7328  ax1rid  7356  axcnre  7360  negid  7673  subneg  7675  negneg  7676  dfinfre  8352  2times  8478  infrenegsupex  9014  rexneg  9224  fseq1p1m1  9438  fzosplitprm1  9573  intfracq  9655  frec2uz0d  9734  frec2uzrdg  9744  frecuzrdg0  9748  frecuzrdgg  9751  frecuzrdg0t  9757  iseqval  9788  iseqvalt  9790  iseqf1olemjpcl  9829  iseqf1olemqpcl  9830  iseqf1olemfvp  9831  iseqf1olemqsum  9834  sqval  9912  iexpcyc  9957  binom3  9968  faclbnd  10046  faclbnd2  10047  bcn1  10063  hashinfom  10083  hashennn  10085  hashxp  10131  shftlem  10147  shftuz  10148  shftidt  10164  reim0  10191  remullem  10201  resqrexlemf1  10337  resqrexlemcalc3  10345  absexpzap  10409  absimle  10413  amgm2  10447  minmax  10556  isummo  10664  fisum  10667  ialgr0  10908  ialgrp1  10910  eucialg  10923  phiprmpw  11080  phiprm  11081  ex-ceil  11099  qdencn  11360
  Copyright terms: Public domain W3C validator