ILE Home 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