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

Theorem 3eqtr2d 2092
Description: A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.)
Hypotheses
Ref Expression
3eqtr2d.1  |-  ( ph  ->  A  =  B )
3eqtr2d.2  |-  ( ph  ->  C  =  B )
3eqtr2d.3  |-  ( ph  ->  C  =  D )
Assertion
Ref Expression
3eqtr2d  |-  ( ph  ->  A  =  D )

Proof of Theorem 3eqtr2d
StepHypRef Expression
1 3eqtr2d.1 . . 3  |-  ( ph  ->  A  =  B )
2 3eqtr2d.2 . . 3  |-  ( ph  ->  C  =  B )
31, 2eqtr4d 2089 . 2  |-  ( ph  ->  A  =  C )
4 3eqtr2d.3 . 2  |-  ( ph  ->  C  =  D )
53, 4eqtrd 2086 1  |-  ( ph  ->  A  =  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1257
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1350  ax-gen 1352  ax-4 1414  ax-17 1433  ax-ext 2036
This theorem depends on definitions:  df-bi 114  df-cleq 2047
This theorem is referenced by:  fmptapd  5379  rdgisucinc  6000  mulidnq  6515  ltrnqg  6546  recexprlem1ssl  6759  recexprlem1ssu  6760  ltmprr  6768  mulcmpblnrlemg  6853  caucvgsrlemoffcau  6910  negsub  7292  neg2sub  7304  divmuleqap  7738  divneg2ap  7757  qapne  8641  binom2  9493  bcpasc  9598  crim  9650  remullem  9663  omeo  10173
  Copyright terms: Public domain W3C validator