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

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

Proof of Theorem eqtr4d
StepHypRef Expression
1 eqtr4d.1 . 2 (φA = B)
2 eqtr4d.2 . . 3 (φ𝐶 = B)
32eqcomd 2023 . 2 (φB = 𝐶)
41, 3eqtrd 2050 1 (φA = 𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1226
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 1312  ax-gen 1314  ax-4 1377  ax-17 1396  ax-ext 2000
This theorem depends on definitions:  df-bi 110  df-cleq 2011
This theorem is referenced by:  3eqtr2d  2056  3eqtr2rd  2057  3eqtr4d  2060  3eqtr4rd  2061  3eqtr4a  2076  sbnfc2  2879  relop  4409  riinint  4516  iotauni  4802  fniinfv  5152  fsn2  5258  fmptapd  5275  fconst2g  5297  fniunfv  5322  ofres  5644  ofco  5648  frecsuclem2  5901  frecrdg  5904  oasuc  5955  nnacom  5974  nnaass  5975  nndi  5976  nnmass  5977  nnmsucr  5978  nnmcom  5979  uniqs2  6073  addcmpblnq  6220  distrnqg  6240  ltexnqq  6260  addcmpblnq0  6292  nqnq0a  6303  nqnq0m  6304  nq0m0r  6305  nq0a0  6306  nnanq0  6307  distrnq0  6308  prarloclemlo  6342  prarloclemcalc  6350  genpassl  6373  genpassu  6374  ltsosr  6505  0idsr  6508  1idsr  6509  cnegex  6776  subsub3  6829  subadd4  6841  mulneg12  6980  mulsub  6984
  Copyright terms: Public domain W3C validator