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

Theorem eqtr4i 2161
Description: An equality transitivity inference. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
eqtr4i.1  |-  A  =  B
eqtr4i.2  |-  C  =  B
Assertion
Ref Expression
eqtr4i  |-  A  =  C

Proof of Theorem eqtr4i
StepHypRef Expression
1 eqtr4i.1 . 2  |-  A  =  B
2 eqtr4i.2 . . 3  |-  C  =  B
32eqcomi 2141 . 2  |-  B  =  C
41, 3eqtri 2158 1  |-  A  =  C
Colors of variables: wff set class
Syntax hints:    = 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 2119
This theorem depends on definitions:  df-bi 116  df-cleq 2130
This theorem is referenced by:  3eqtr2i  2164  3eqtr2ri  2165  3eqtr4i  2168  3eqtr4ri  2169  rabab  2702  cbvralcsf  3057  cbvrexcsf  3058  cbvrabcsf  3060  dfin5  3073  dfdif2  3074  uneqin  3322  unrab  3342  inrab  3343  inrab2  3344  difrab  3345  dfrab3ss  3349  rabun2  3350  difidALT  3427  difdifdirss  3442  dfif3  3482  tpidm  3620  dfint2  3768  iunrab  3855  uniiun  3861  intiin  3862  0iin  3866  mptv  4020  xpundi  4590  xpundir  4591  resiun2  4834  resopab  4858  opabresid  4867  dfse2  4907  cnvun  4939  cnvin  4941  imaundir  4947  imainrect  4979  cnvcnv2  4987  cnvcnvres  4997  dmtpop  5009  rnsnopg  5012  rnco2  5041  dmco  5042  co01  5048  unidmrn  5066  dfdm2  5068  funimaexg  5202  dfmpt3  5240  mptun  5249  funcocnv2  5385  fnasrn  5591  fnasrng  5593  fpr  5595  fmptap  5603  riotav  5728  dmoprab  5845  rnoprab2  5848  mpov  5854  mpomptx  5855  abrexex2g  6011  abrexex2  6015  1stval2  6046  2ndval2  6047  fo1st  6048  fo2nd  6049  xp2  6064  dfoprab4f  6084  fmpoco  6106  tposmpo  6171  recsfval  6205  frecfnom  6291  freccllem  6292  frecfcllem  6294  frecsuclem  6296  df2o3  6320  o1p1e2  6357  ecqs  6484  qliftf  6507  erovlem  6514  mapsnf1o3  6584  ixp0x  6613  xpf1o  6731  djuunr  6944  dmaddpq  7180  dmmulpq  7181  enq0enq  7232  nqprlu  7348  m1p1sr  7561  m1m1sr  7562  caucvgsr  7603  dfcnqs  7642  3m1e2  8833  2p2e4  8840  3p2e5  8854  3p3e6  8855  4p2e6  8856  4p3e7  8857  4p4e8  8858  5p2e7  8859  5p3e8  8860  5p4e9  8861  6p2e8  8862  6p3e9  8863  7p2e9  8864  nn0supp  9022  nnzrab  9071  nn0zrab  9072  dec0u  9195  dec0h  9196  decsuc  9205  decsucc  9215  numma  9218  decma  9225  decmac  9226  decma2c  9227  decadd  9228  decaddc  9229  decmul1  9238  decmul1c  9239  decmul2c  9240  5p5e10  9245  6p4e10  9246  7p3e10  9249  8p2e10  9254  5t5e25  9277  6t6e36  9282  8t6e48  9293  nn0uz  9353  nnuz  9354  xaddcom  9637  ioomax  9724  iccmax  9725  ioopos  9726  ioorp  9727  fseq1p1m1  9867  fzo0to2pr  9988  fzo0to3tp  9989  frecfzennn  10192  irec  10385  sq10e99m1  10453  facnn  10466  fac0  10467  faclbnd2  10481  zfz1isolemsplit  10574  minmax  10994  xrminmax  11027  fisumrev2  11208  fsumparts  11232  fsumiun  11239  isumnn0nn  11255  ege2le3  11366  cos1bnd  11455  efieq1re  11467  eirraplem  11472  phiprmpw  11887  unennn  11899  ennnfonelemjn  11904  qnnen  11933  strle1g  12038  tgrest  12327  uniretop  12683  dvexp  12833  dvef  12845  cospi  12870  sincos6thpi  12912  bj-omind  13121
  Copyright terms: Public domain W3C validator