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

Theorem syl5eq 2081
Description: An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl5eq.1 A = B
syl5eq.2 (φB = 𝐶)
Assertion
Ref Expression
syl5eq (φA = 𝐶)

Proof of Theorem syl5eq
StepHypRef Expression
1 syl5eq.1 . . 3 A = B
21a1i 9 . 2 (φA = B)
3 syl5eq.2 . 2 (φB = 𝐶)
42, 3eqtrd 2069 1 (φA = 𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1242
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-gen 1335  ax-4 1397  ax-17 1416  ax-ext 2019
This theorem depends on definitions:  df-bi 110  df-cleq 2030
This theorem is referenced by:  syl5req  2082  syl5eqr  2083  3eqtr3a  2093  3eqtr4g  2094  csbtt  2856  csbvarg  2871  csbie2g  2890  rabbi2dva  3139  csbprc  3256  disjssun  3279  disjpr2  3425  prprc2  3470  difprsn2  3495  opprc  3561  intsng  3640  riinm  3720  iinxsng  3721  rintm  3735  sucprc  4115  unisucg  4117  xpriindim  4417  relop  4429  dmxpm  4498  riinint  4536  resabs1  4583  resabs2  4584  resima2  4587  xpssres  4588  resopab2  4598  imasng  4633  ndmima  4645  xpdisj1  4690  xpdisj2  4691  djudisj  4693  resdisj  4694  rnxpm  4695  xpima1  4710  xpima2m  4711  dmsnsnsng  4741  rnsnopg  4742  rnpropg  4743  mptiniseg  4758  dfco2a  4764  relcoi1  4792  unixpm  4796  iotaval  4821  funtp  4895  fnun  4948  fnresdisj  4952  fnima  4960  fnimaeq0  4963  fcoi1  5013  f1orescnv  5085  foun  5088  resdif  5091  tz6.12-2  5112  fveu  5113  tz6.12-1  5143  fvun2  5183  fvopab3ig  5189  f1oresrab  5272  dfmptg  5285  ressnop0  5287  fvunsng  5300  fsnunfv  5306  fvpr1  5308  fvpr2  5309  fvpr1g  5310  fvpr2g  5311  fvtp1g  5312  fvtp2g  5313  fvtp3g  5314  fvtp2  5316  fvtp3  5317  f1oiso2  5409  riotaund  5445  ovprc  5482  resoprab2  5540  fnoprabg  5544  ovidig  5560  ovigg  5563  ov6g  5580  ovconst2  5594  offval2  5668  ot1stg  5721  ot2ndg  5722  ot3rdgg  5723  fmpt2co  5779  tpostpos2  5821  rdgisuc1  5911  frec0g  5922  frecsuclem1  5926  frecsuclem2  5928  frecrdg  5931  oasuc  5983  oa1suc  5986  omsuc  5990  nnm1  6033  nnm2  6034  dfec2  6045  errn  6064  1qec  6372  mulidnq  6373  addpinq1  6446  0idsr  6655  1idsr  6656  mulresr  6695  pitonnlem2  6703  ax1rid  6721  axcnre  6725  negid  7014  subneg  7016  negneg  7017  2times  7776  rexneg  8473  fseq1p1m1  8686  fzosplitprm1  8820  frec2uz0d  8826  frec2uzrdg  8836  frecuzrdg0  8841  iseqval  8860  sqval  8926  binom3  8979  reim0  9049  remullem  9059
  Copyright terms: Public domain W3C validator