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

Theorem eqtr3d 2071
Description: An equality transitivity equality deduction. (Contributed by NM, 18-Jul-1995.)
Hypotheses
Ref Expression
eqtr3d.1 (φA = B)
eqtr3d.2 (φA = 𝐶)
Assertion
Ref Expression
eqtr3d (φB = 𝐶)

Proof of Theorem eqtr3d
StepHypRef Expression
1 eqtr3d.1 . . 3 (φA = B)
21eqcomd 2042 . 2 (φB = A)
3 eqtr3d.2 . 2 (φA = 𝐶)
42, 3eqtrd 2069 1 (φB = 𝐶)
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:  3eqtr3d  2077  3eqtr3rd  2078  3eqtr3a  2093  opth  3965  eusvnf  4151  f00  5024  f1imacnv  5086  foimacnv  5087  f1ococnv1  5098  funfvdm  5179  fvmptdf  5201  fndmdif  5215  acexmidlemph  5448  acexmidlemab  5449  ovmpt2df  5574  oprssov  5584  grpridd  5639  tfrlemisucaccv  5880  oav2  5982  omv2  5984  ecopovtrn  6139  ecopovtrng  6142  en1  6215  distrnqg  6371  1qec  6372  prarloclemarch2  6402  nnnq0lem1  6429  nqpnq0nq  6436  distrnq0  6442  prarloclemlt  6476  prmuloclemcalc  6546  ltaprg  6592  recexprlem1ssl  6605  recexprlem1ssu  6606  ltmprr  6614  cauappcvgprlemopl  6618  caucvgprlemopl  6640  prsrlem1  6670  ltsosr  6692  mulgt0sr  6704  addid2  6949  readdcan  6950  add32r  6968  cnegexlem2  6984  cnegex  6986  pncan2  7015  addsubass  7018  subadd23  7020  addsub12  7021  subid  7026  subid1  7027  npncan  7028  nppcan3  7031  subsub  7037  nppcan2  7038  nnncan2  7044  npncan3  7045  pnpcan  7046  negdi  7064  subdi  7178  mulsub  7194  mulsub2  7195  recexap  7416  div32ap  7453  divsubdirap  7466  divmuldivap  7470  divdivdivap  7471  divmuleqap  7475  divcanap6  7477  dmdcanap  7480  divsubdivap  7486  div2negap  7493  mvllmulapd  7590  prodgt0gt0  7598  cju  7694  zneo  8115  qreccl  8351  fzosn  8831  expineg2  8918  expm1t  8937  expadd  8951  expaddzaplem  8952  expmulzap  8955  sqsubswap  8968  subsq2  9012  binom2sub  9017  binom3  9019  reim0  9089  imval2  9122  cjreim2  9132  cjdivap  9137  cnrecnv  9138  rennim  9211  sqrtmsq  9215  absnid  9227
  Copyright terms: Public domain W3C validator