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

Theorem eqtr4d 2072
Description: An equality transitivity equality deduction. (Contributed by NM, 18-Jul-1995.)
Hypotheses
Ref Expression
eqtr4d.1 (φA = B)
eqtr4d.2 (φ𝐶 = B)
Assertion
Ref Expression
eqtr4d (φA = 𝐶)

Proof of Theorem eqtr4d
StepHypRef Expression
1 eqtr4d.1 . 2 (φA = B)
2 eqtr4d.2 . . 3 (φ𝐶 = B)
32eqcomd 2042 . 2 (φB = 𝐶)
41, 3eqtrd 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:  3eqtr2d  2075  3eqtr2rd  2076  3eqtr4d  2079  3eqtr4rd  2080  3eqtr4a  2095  sbnfc2  2900  relop  4429  riinint  4536  iotauni  4822  fniinfv  5174  fsn2  5280  fmptapd  5297  fconst2g  5319  fniunfv  5344  ofres  5667  ofco  5671  frecsuclem2  5928  frecrdg  5931  oasuc  5983  nnacom  6002  nnaass  6003  nndi  6004  nnmass  6005  nnmsucr  6006  nnmcom  6007  uniqs2  6102  en1bg  6216  fundmen  6222  addcmpblnq  6351  distrnqg  6371  ltexnqq  6391  addcmpblnq0  6425  nqnq0a  6436  nqnq0m  6437  nq0m0r  6438  nq0a0  6439  nnanq0  6440  distrnq0  6441  prarloclemlo  6476  prarloclemcalc  6484  genpassl  6507  genpassu  6508  ltsosr  6652  0idsr  6655  1idsr  6656  mulextsr1lem  6666  cnegex  6946  subsub3  6999  subadd4  7011  mulneg12  7150  mulsub  7154  apreap  7331  cru  7346  recextlem1  7374  cju  7654  halfaddsub  7896  nn0supp  7970  nneo  8077  zeo2  8080  uzin  8241  iccf1o  8602  fzsuc2  8671  frec2uzrdg  8836  iseqfveq2  8865  expp1  8876  mulexp  8908  mulexpzap  8909  expadd  8911  expaddzap  8913  expmul  8914  expmulzap  8915  expsubap  8916  expdivap  8919  subsq  8971  binom3  8979  bernneq  8982  crre  9045  remim  9048  remullem  9059  cjexp  9081  cnrecnv  9098
  Copyright terms: Public domain W3C validator