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  6676  cnegexlem3  6965  cnegex  6966  submul2  7172  mulsubfacd  7191  divadddivap  7465  fzval3  8810  fzoshftral  8844  frecuzrdgfn  8859  expnegzap  8923  binom2sub  8997  binom3  8999  reim  9060  mulreap  9072  addcj  9099
  Copyright terms: Public domain W3C validator