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

Theorem syl6eqr 2403
 Description: An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl6eqr.1 (φA = B)
syl6eqr.2 C = B
Assertion
Ref Expression
syl6eqr (φA = C)

Proof of Theorem syl6eqr
StepHypRef Expression
1 syl6eqr.1 . 2 (φA = B)
2 syl6eqr.2 . . 3 C = B
32eqcomi 2357 . 2 B = C
41, 3syl6eq 2401 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:  3eqtr4g  2410  iinrab2  4029  setswith  4321  pw1equn  4331  uniabio  4349  iotanul  4354  nnsucelrlem3  4426  ltfintr  4459  lefinlteq  4463  sfinltfin  4535  1cvsfin  4542  tncveqnc1fin  4544  phialllem1  4616  phialllem2  4617  dfimafn2  5367  fnasrn  5417  ffnov  5587  fnov  5591  fnrnov  5605  foov  5606  funimassov  5609  ovelimab  5610  fce  6188  ce0  6190  el2c  6191  nc0le1  6216  nclenn  6249  ncslesuc  6267  nchoicelem9  6297
 Copyright terms: Public domain W3C validator