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

Theorem 3eqtr3rd 2181
 Description: A deduction from three chained equalities. (Contributed by NM, 14-Jan-2006.)
Hypotheses
Ref Expression
3eqtr3d.1 (𝜑𝐴 = 𝐵)
3eqtr3d.2 (𝜑𝐴 = 𝐶)
3eqtr3d.3 (𝜑𝐵 = 𝐷)
Assertion
Ref Expression
3eqtr3rd (𝜑𝐷 = 𝐶)

Proof of Theorem 3eqtr3rd
StepHypRef Expression
1 3eqtr3d.3 . 2 (𝜑𝐵 = 𝐷)
2 3eqtr3d.1 . . 3 (𝜑𝐴 = 𝐵)
3 3eqtr3d.2 . . 3 (𝜑𝐴 = 𝐶)
42, 3eqtr3d 2174 . 2 (𝜑𝐵 = 𝐶)
51, 4eqtr3d 2174 1 (𝜑𝐷 = 𝐶)
 Colors of variables: wff set class Syntax hints:   → wi 4   = wceq 1331 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 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2121 This theorem depends on definitions:  df-bi 116  df-cleq 2132 This theorem is referenced by:  fcofo  5685  fcof1o  5690  frecabcl  6296  nnaword  6407  enomnilem  7010  fodju0  7019  pn0sr  7586  negeu  7960  add20  8243  2halves  8956  bcnn  10510  bcpasc  10519  resqrexlemover  10789  fsumneg  11227  geolim  11287  geolim2  11288  mertensabs  11313  sincossq  11462  demoivre  11486  eirraplem  11490  gcdid  11681  gcdmultipled  11688  phiprmpw  11905  ioo2bl  12722  ptolemy  12915  coskpi  12939
 Copyright terms: Public domain W3C validator