NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  eqtr4d GIF version

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

Proof of Theorem eqtr4d
StepHypRef Expression
1 eqtr4d.1 . 2 (φA = B)
2 eqtr4d.2 . . 3 (φC = B)
32eqcomd 2358 . 2 (φB = C)
41, 3eqtrd 2385 1 (φA = C)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1642
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746  ax-ext 2334
This theorem depends on definitions:  df-bi 177  df-ex 1542  df-cleq 2346
This theorem is referenced by:  3eqtr2d  2391  3eqtr2rd  2392  3eqtr4d  2395  3eqtr4rd  2396  3eqtr4a  2411  sbnfc2  3196  ifsb  3671  ifeq1da  3687  ifeq2da  3688  ifnot  3700  ifan  3701  ifor  3702  setswith  4321  iotauni  4351  dfiota3  4370  dfiota4  4372  nnsucelrlem3  4426  nnpw1ex  4484  tfin11  4493  sfin112  4529  fveqres  5355  funfv  5375  fsn2  5434  fvunsn  5444  fconst2g  5452  ndmovcom  5617  ndmovass  5618  ndmovdistr  5619  fvmpti  5699  fvmptex  5721  fvfullfun  5864  uniqs2  5985  enprmaplem3  6078  nchoicelem7  6295  nchoicelem15  6303  nchoicelem17  6305  fnfrec  6320
  Copyright terms: Public domain W3C validator