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

Theorem eqtr2d 2073
 Description: An equality transitivity deduction. (Contributed by NM, 18-Oct-1999.)
Hypotheses
Ref Expression
eqtr2d.1 (𝜑𝐴 = 𝐵)
eqtr2d.2 (𝜑𝐵 = 𝐶)
Assertion
Ref Expression
eqtr2d (𝜑𝐶 = 𝐴)

Proof of Theorem eqtr2d
StepHypRef Expression
1 eqtr2d.1 . . 3 (𝜑𝐴 = 𝐵)
2 eqtr2d.2 . . 3 (𝜑𝐵 = 𝐶)
31, 2eqtrd 2072 . 2 (𝜑𝐴 = 𝐶)
43eqcomd 2045 1 (𝜑𝐶 = 𝐴)
 Colors of variables: wff set class Syntax hints:   → wi 4   = wceq 1243 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 1336  ax-gen 1338  ax-4 1400  ax-17 1419  ax-ext 2022 This theorem depends on definitions:  df-bi 110  df-cleq 2033 This theorem is referenced by:  3eqtrrd  2077  3eqtr2rd  2079  onsucmin  4233  elxp4  4808  elxp5  4809  csbopeq1a  5814  ecinxp  6181  fundmen  6286  fidifsnen  6331  addpinq1  6562  1idsr  6853  prsradd  6870  cnegexlem3  7188  cnegex  7189  submul2  7396  mulsubfacd  7415  divadddivap  7703  fzval3  9060  fzoshftral  9094  ceiqm1l  9153  flqdiv  9163  flqmod  9180  intqfrac  9181  frecuzrdgfn  9198  expnegzap  9289  binom2sub  9364  binom3  9366  reim  9452  mulreap  9464  addcj  9491  resqrexlemcalc1  9612  absimle  9680  clim2iser  9857  serif0  9871
 Copyright terms: Public domain W3C validator