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

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

Proof of Theorem eqtr2d
StepHypRef Expression
1 eqtr2d.1 . . 3
2 eqtr2d.2 . . 3  C
31, 2eqtrd 2069 . 2  C
43eqcomd 2042 1  C
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  6447  1idsr  6696  cnegexlem3  6985  cnegex  6986  submul2  7192  mulsubfacd  7211  divadddivap  7485  fzval3  8830  fzoshftral  8864  frecuzrdgfn  8879  expnegzap  8943  binom2sub  9017  binom3  9019  reim  9080  mulreap  9092  addcj  9119
  Copyright terms: Public domain W3C validator