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

Theorem eqtr3d 2074
Description: An equality transitivity equality deduction. (Contributed by NM, 18-Jul-1995.)
Hypotheses
Ref Expression
eqtr3d.1  |-  ( ph  ->  A  =  B )
eqtr3d.2  |-  ( ph  ->  A  =  C )
Assertion
Ref Expression
eqtr3d  |-  ( ph  ->  B  =  C )

Proof of Theorem eqtr3d
StepHypRef Expression
1 eqtr3d.1 . . 3  |-  ( ph  ->  A  =  B )
21eqcomd 2045 . 2  |-  ( ph  ->  B  =  A )
3 eqtr3d.2 . 2  |-  ( ph  ->  A  =  C )
42, 3eqtrd 2072 1  |-  ( ph  ->  B  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1243
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 1336  ax-gen 1338  ax-4 1400  ax-17 1419  ax-ext 2022
This theorem depends on definitions:  df-bi 110  df-cleq 2033
This theorem is referenced by:  3eqtr3d  2080  3eqtr3rd  2081  3eqtr3a  2096  opth  3974  eusvnf  4185  f00  5081  f1imacnv  5143  foimacnv  5144  f1ococnv1  5155  funfvdm  5236  fvmptdf  5258  fndmdif  5272  acexmidlemph  5505  acexmidlemab  5506  ovmpt2df  5632  oprssov  5642  grpridd  5697  tfrlemisucaccv  5939  oav2  6043  omv2  6045  ecopovtrn  6203  ecopovtrng  6206  en1  6279  fidifsnen  6331  dif1en  6337  ordiso2  6355  distrnqg  6483  1qec  6484  prarloclemarch2  6515  nnnq0lem1  6542  nqpnq0nq  6549  distrnq0  6555  prarloclemlt  6589  prmuloclemcalc  6661  ltaprg  6715  prplnqu  6716  recexprlem1ssl  6729  recexprlem1ssu  6730  ltmprr  6738  cauappcvgprlemopl  6742  caucvgprlemopl  6765  caucvgprprlemopl  6793  caucvgprprlemexb  6803  prsrlem1  6825  ltsosr  6847  mulgt0sr  6860  recidpipr  6930  recriota  6962  nntopi  6966  axcaucvglemres  6971  addid2  7150  readdcan  7151  add32r  7169  cnegexlem2  7185  cnegex  7187  pncan2  7216  addsubass  7219  subadd23  7221  addsub12  7222  subid  7228  subid1  7229  npncan  7230  nppcan3  7233  subsub  7239  nppcan2  7240  nnncan2  7246  npncan3  7247  pnpcan  7248  negdi  7266  subdi  7380  mulsub  7396  mulsub2  7397  recexap  7632  div32ap  7669  divsubdirap  7682  divmuldivap  7686  divdivdivap  7687  divmuleqap  7691  divcanap6  7693  dmdcanap  7696  divsubdivap  7702  div2negap  7709  mvllmulapd  7807  prodgt0gt0  7815  cju  7911  zneo  8337  qreccl  8574  fzosn  9059  iseqdistr  9223  expineg2  9238  expm1t  9257  expadd  9271  expaddzaplem  9272  expmulzap  9275  sqsubswap  9288  subsq2  9333  binom2sub  9338  binom3  9340  2shfti  9406  shftcan2  9410  reim0  9435  imval2  9468  cjreim2  9478  cjdivap  9483  cnrecnv  9484  rennim  9574  resqrexlemnm  9590  remsqsqrt  9604  sqrtdiv  9614  sqrtmsq  9617  sqabsadd  9627  sqabssub  9628  absreim  9640  absdivap  9642  absnid  9645  sqabs  9652  abslt  9658  absle  9659  recvalap  9667  abssub  9671  mulcn2  9807  cjcn2  9810  sqr2irrlem  9851  ialgcvg  9861
  Copyright terms: Public domain W3C validator