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

Theorem eqtr4d 2091
Description: An equality transitivity equality deduction. (Contributed by NM, 18-Jul-1995.)
Hypotheses
Ref Expression
eqtr4d.1  |-  ( ph  ->  A  =  B )
eqtr4d.2  |-  ( ph  ->  C  =  B )
Assertion
Ref Expression
eqtr4d  |-  ( ph  ->  A  =  C )

Proof of Theorem eqtr4d
StepHypRef Expression
1 eqtr4d.1 . 2  |-  ( ph  ->  A  =  B )
2 eqtr4d.2 . . 3  |-  ( ph  ->  C  =  B )
32eqcomd 2061 . 2  |-  ( ph  ->  B  =  C )
41, 3eqtrd 2088 1  |-  ( ph  ->  A  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1259
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-4 1416  ax-17 1435  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-cleq 2049
This theorem is referenced by:  3eqtr2d  2094  3eqtr2rd  2095  3eqtr4d  2098  3eqtr4rd  2099  3eqtr4a  2114  sbnfc2  2934  onsucuni2  4316  relop  4514  riinint  4621  iotauni  4907  fniinfv  5259  fsn2  5365  fmptapd  5382  fconst2g  5404  fniunfv  5429  ofres  5753  ofco  5757  frecsuclem2  6020  frecrdg  6023  oasuc  6075  nnacom  6094  nnaass  6095  nndi  6096  nnmass  6097  nnmsucr  6098  nnmcom  6099  uniqs2  6197  en1bg  6311  fundmen  6317  phplem4dom  6355  addcmpblnq  6523  distrnqg  6543  ltexnqq  6564  addcmpblnq0  6599  nqnq0a  6610  nqnq0m  6611  nq0m0r  6612  nq0a0  6613  nnanq0  6614  distrnq0  6615  prarloclemlo  6650  prarloclemcalc  6658  genpassl  6680  genpassu  6681  ltsosr  6907  0idsr  6910  1idsr  6911  mulextsr1lem  6922  cnegex  7252  subsub3  7306  subadd4  7318  mulneg12  7466  mulsub  7470  apreap  7652  cru  7667  recextlem1  7706  cju  7989  halfaddsub  8216  nn0supp  8291  nneo  8400  zeo2  8403  uzin  8601  iccf1o  8973  fzsuc2  9043  flqeqceilz  9268  zmod1congr  9291  modqcyc  9309  modqcyc2  9310  modqaddabs  9312  modqmul1  9327  modqaddmulmod  9341  addmodlteq  9348  frec2uzrdg  9359  iseqss  9390  iseqfveq2  9392  iseqsplit  9402  iseqdistr  9414  iser0f  9416  expp1  9427  mulexp  9459  mulexpzap  9460  expadd  9462  expaddzap  9464  expmul  9465  expmulzap  9466  expsubap  9468  expdivap  9471  subsq  9525  mulbinom2  9533  binom3  9534  bernneq  9537  nn0opthd  9590  faclbnd  9609  faclbnd6  9612  bccmpl  9622  bcp1n  9629  shftval2  9655  shftval4  9657  crre  9685  remim  9688  remullem  9699  cjexp  9721  cnrecnv  9738  resqrexlemlo  9840  resqrexlemcalc1  9841  resqrexlemcalc2  9842  resqrexlemcalc3  9843  resqrexlemnm  9845  rsqrmo  9854  abscj  9879  absid  9898  absre  9904  recvalap  9924  climaddc1  10080  climmulc2  10082  climsubc1  10083  climsubc2  10084  climcvg1nlem  10099  odd2np1  10184  omoe  10208  divalglemex  10234  divalglemeuneg  10235  divalgmod  10239  flodddiv4  10246  sqrt2irr  10251  ialgrp1  10268
  Copyright terms: Public domain W3C validator