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

Theorem 3eqtr2d 2120
 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 2117 . 2 (𝜑𝐴 = 𝐶)
4 3eqtr2d.3 . 2 (𝜑𝐶 = 𝐷)
53, 4eqtrd 2114 1 (𝜑𝐴 = 𝐷)
 Colors of variables: wff set class Syntax hints:   → wi 4   = wceq 1285 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-4 1441  ax-17 1460  ax-ext 2064 This theorem depends on definitions:  df-bi 115  df-cleq 2075 This theorem is referenced by:  fmptapd  5380  rdgisucinc  6028  mulidnq  6630  ltrnqg  6661  recexprlem1ssl  6874  recexprlem1ssu  6875  ltmprr  6883  mulcmpblnrlemg  6968  caucvgsrlemoffcau  7025  negsub  7412  neg2sub  7424  divmuleqap  7861  divneg2ap  7880  qapne  8794  binom2  9671  bcpasc  9779  crim  9872  remullem  9885  max0addsup  10232  omeo  10431  sqgcd  10551
 Copyright terms: Public domain W3C validator