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

Theorem 3eqtr2d 2078
 Description: A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.)
Hypotheses
Ref Expression
3eqtr2d.1
3eqtr2d.2
3eqtr2d.3
Assertion
Ref Expression
3eqtr2d

Proof of Theorem 3eqtr2d
StepHypRef Expression
1 3eqtr2d.1 . . 3
2 3eqtr2d.2 . . 3
31, 2eqtr4d 2075 . 2
4 3eqtr2d.3 . 2
53, 4eqtrd 2072 1
 Colors of variables: wff set class Syntax hints:   wi 4   wceq 1243 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 1336  ax-gen 1338  ax-4 1400  ax-17 1419  ax-ext 2022 This theorem depends on definitions:  df-bi 110  df-cleq 2033 This theorem is referenced by:  fmptapd  5354  rdgisucinc  5972  mulidnq  6487  ltrnqg  6518  recexprlem1ssl  6731  recexprlem1ssu  6732  ltmprr  6740  mulcmpblnrlemg  6825  caucvgsrlemoffcau  6882  negsub  7259  neg2sub  7271  divmuleqap  7693  divneg2ap  7712  qapne  8574  binom2  9362  crim  9458  remullem  9471
 Copyright terms: Public domain W3C validator