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

Theorem 3eqtr2d 2133
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 2130 . 2 (𝜑𝐴 = 𝐶)
4 3eqtr2d.3 . 2 (𝜑𝐶 = 𝐷)
53, 4eqtrd 2127 1 (𝜑𝐴 = 𝐷)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1296
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1388  ax-gen 1390  ax-4 1452  ax-17 1471  ax-ext 2077
This theorem depends on definitions:  df-bi 116  df-cleq 2088
This theorem is referenced by:  fmptapd  5527  rdgisucinc  6188  ctm  6871  mulidnq  7045  ltrnqg  7076  recexprlem1ssl  7289  recexprlem1ssu  7290  ltmprr  7298  mulcmpblnrlemg  7383  caucvgsrlemoffcau  7440  negsub  7827  neg2sub  7839  divmuleqap  8281  divneg2ap  8300  qapne  9223  binom2  10180  bcpasc  10289  crim  10407  remullem  10420  max0addsup  10767  summodclem2a  10924  isum1p  11035  geo2sum  11057  cvgratz  11075  efi4p  11157  tanaddap  11179  addcos  11186  cos2tsin  11191  demoivreALT  11212  omeo  11325  sqgcd  11445
  Copyright terms: Public domain W3C validator