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

Theorem eqtr2d 2070
Description: An equality transitivity deduction. (Contributed by NM, 18-Oct-1999.)
Hypotheses
Ref Expression
eqtr2d.1 (φA = B)
eqtr2d.2 (φB = 𝐶)
Assertion
Ref Expression
eqtr2d (φ𝐶 = A)

Proof of Theorem eqtr2d
StepHypRef Expression
1 eqtr2d.1 . . 3 (φA = B)
2 eqtr2d.2 . . 3 (φB = 𝐶)
31, 2eqtrd 2069 . 2 (φA = 𝐶)
43eqcomd 2042 1 (φ𝐶 = A)
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:  3eqtrrd  2074  3eqtr2rd  2076  onsucmin  4198  elxp4  4751  elxp5  4752  csbopeq1a  5756  ecinxp  6117  fundmen  6222  addpinq1  6446  1idsr  6656  cnegexlem3  6945  cnegex  6946  submul2  7152  mulsubfacd  7171  divadddivap  7445  fzval3  8790  fzoshftral  8824  frecuzrdgfn  8839  expnegzap  8903  binom2sub  8977  binom3  8979  reim  9040  mulreap  9052  addcj  9079
  Copyright terms: Public domain W3C validator