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

Theorem 3eqtr2d 2156
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 2153 . 2  |-  ( ph  ->  A  =  C )
4 3eqtr2d.3 . 2  |-  ( ph  ->  C  =  D )
53, 4eqtrd 2150 1  |-  ( ph  ->  A  =  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1316
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1408  ax-gen 1410  ax-4 1472  ax-17 1491  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-cleq 2110
This theorem is referenced by:  fmptapd  5579  rdgisucinc  6250  ctm  6962  mulidnq  7165  ltrnqg  7196  recexprlem1ssl  7409  recexprlem1ssu  7410  ltmprr  7418  mulcmpblnrlemg  7516  caucvgsrlemoffcau  7574  negsub  7978  neg2sub  7990  divmuleqap  8445  divneg2ap  8464  qapne  9399  seqvalcd  10200  binom2  10371  bcpasc  10480  crim  10598  remullem  10611  max0addsup  10959  summodclem2a  11118  isum1p  11229  geo2sum  11251  cvgratz  11269  efi4p  11351  tanaddap  11373  addcos  11380  cos2tsin  11385  demoivreALT  11407  omeo  11522  sqgcd  11644  txrest  12372  limccnpcntop  12740  dvrecap  12773  cosq34lt1  12858
  Copyright terms: Public domain W3C validator