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  6428  nqpnq0nq  6435  distrnq0  6441  prarloclemlt  6475  prmuloclemcalc  6544  ltaprg  6590  recexprlem1ssl  6603  recexprlem1ssu  6604  ltmprr  6612  prsrlem1  6630  ltsosr  6652  mulgt0sr  6664  addid2  6909  readdcan  6910  add32r  6928  cnegexlem2  6944  cnegex  6946  pncan2  6975  addsubass  6978  subadd23  6980  addsub12  6981  subid  6986  subid1  6987  npncan  6988  nppcan3  6991  subsub  6997  nppcan2  6998  nnncan2  7004  npncan3  7005  pnpcan  7006  negdi  7024  subdi  7138  mulsub  7154  mulsub2  7155  recexap  7376  div32ap  7413  divsubdirap  7426  divmuldivap  7430  divdivdivap  7431  divmuleqap  7435  divcanap6  7437  dmdcanap  7440  divsubdivap  7446  div2negap  7453  mvllmulapd  7550  prodgt0gt0  7558  cju  7654  zneo  8075  qreccl  8311  fzosn  8791  expineg2  8878  expm1t  8897  expadd  8911  expaddzaplem  8912  expmulzap  8915  sqsubswap  8928  subsq2  8972  binom2sub  8977  binom3  8979  reim0  9049  imval2  9082  cjreim2  9092  cjdivap  9097  cnrecnv  9098
  Copyright terms: Public domain W3C validator