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

Theorem 3eqtr2d 2075
Description: A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.)
Hypotheses
Ref Expression
3eqtr2d.1 (φA = B)
3eqtr2d.2 (φ𝐶 = B)
3eqtr2d.3 (φ𝐶 = 𝐷)
Assertion
Ref Expression
3eqtr2d (φA = 𝐷)

Proof of Theorem 3eqtr2d
StepHypRef Expression
1 3eqtr2d.1 . . 3 (φA = B)
2 3eqtr2d.2 . . 3 (φ𝐶 = B)
31, 2eqtr4d 2072 . 2 (φA = 𝐶)
4 3eqtr2d.3 . 2 (φ𝐶 = 𝐷)
53, 4eqtrd 2069 1 (φA = 𝐷)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1242
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-gen 1335  ax-4 1397  ax-17 1416  ax-ext 2019
This theorem depends on definitions:  df-bi 110  df-cleq 2030
This theorem is referenced by:  fmptapd  5297  rdgisucinc  5912  mulidnq  6373  ltrnqg  6403  recexprlem1ssl  6603  recexprlem1ssu  6604  ltmprr  6612  mulcmpblnrlemg  6628  negsub  7015  neg2sub  7027  divmuleqap  7435  divneg2ap  7454  qapne  8310  binom2  8975  crim  9046  remullem  9059
  Copyright terms: Public domain W3C validator