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

Theorem 3eqtr2d 2179
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 2176 . 2 (𝜑𝐴 = 𝐶)
4 3eqtr2d.3 . 2 (𝜑𝐶 = 𝐷)
53, 4eqtrd 2173 1 (𝜑𝐴 = 𝐷)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1332
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 1424  ax-gen 1426  ax-4 1488  ax-17 1507  ax-ext 2122
This theorem depends on definitions:  df-bi 116  df-cleq 2133
This theorem is referenced by:  fmptapd  5618  rdgisucinc  6289  ctm  7001  mulidnq  7220  ltrnqg  7251  recexprlem1ssl  7464  recexprlem1ssu  7465  ltmprr  7473  mulcmpblnrlemg  7571  caucvgsrlemoffcau  7629  negsub  8033  neg2sub  8045  divmuleqap  8500  divneg2ap  8519  qapne  9457  seqvalcd  10262  binom2  10433  bcpasc  10543  crim  10661  remullem  10674  max0addsup  11022  summodclem2a  11181  isum1p  11292  geo2sum  11314  cvgratz  11332  efi4p  11458  tanaddap  11480  addcos  11487  cos2tsin  11492  demoivreALT  11514  omeo  11629  sqgcd  11751  txrest  12482  limccnpcntop  12850  dvrecap  12883  cosq34lt1  12977
  Copyright terms: Public domain W3C validator