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

Theorem 3eqtr3rd 2136
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 2129 . 2 (𝜑𝐵 = 𝐶)
51, 4eqtr3d 2129 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:  fcofo  5601  fcof1o  5606  frecabcl  6202  nnaword  6310  enomnilem  6881  fodju0  6890  pn0sr  7414  negeu  7770  add20  8049  2halves  8743  bcnn  10280  bcpasc  10289  resqrexlemover  10558  fsumneg  10994  geolim  11054  geolim2  11055  mertensabs  11080  sincossq  11188  demoivre  11211  eirraplem  11213  gcdid  11404  phiprmpw  11625  ioo2bl  12319
  Copyright terms: Public domain W3C validator