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

Theorem eqtr4i 2105
Description: An equality transitivity inference. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
eqtr4i.1 𝐴 = 𝐵
eqtr4i.2 𝐶 = 𝐵
Assertion
Ref Expression
eqtr4i 𝐴 = 𝐶

Proof of Theorem eqtr4i
StepHypRef Expression
1 eqtr4i.1 . 2 𝐴 = 𝐵
2 eqtr4i.2 . . 3 𝐶 = 𝐵
32eqcomi 2086 . 2 𝐵 = 𝐶
41, 3eqtri 2102 1 𝐴 = 𝐶
Colors of variables: wff set class
Syntax hints:   = wceq 1285
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-4 1441  ax-17 1460  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-cleq 2075
This theorem is referenced by:  3eqtr2i  2108  3eqtr2ri  2109  3eqtr4i  2112  3eqtr4ri  2113  rabab  2621  cbvralcsf  2965  cbvrexcsf  2966  cbvrabcsf  2968  dfin5  2981  dfdif2  2982  uneqin  3222  unrab  3242  inrab  3243  inrab2  3244  difrab  3245  dfrab3ss  3249  rabun2  3250  difidALT  3320  difdifdirss  3334  dfif3  3372  tpidm  3502  dfint2  3646  iunrab  3733  uniiun  3739  intiin  3740  0iin  3744  mptv  3882  xpundi  4422  xpundir  4423  resiun2  4659  resopab  4682  opabresid  4689  dfse2  4728  cnvun  4759  cnvin  4761  imaundir  4767  imainrect  4796  cnvcnv2  4804  cnvcnvres  4814  dmtpop  4826  rnsnopg  4829  rnco2  4858  dmco  4859  co01  4865  unidmrn  4880  dfdm2  4882  funimaexg  5014  dfmpt3  5052  mptun  5060  funcocnv2  5182  fnasrn  5373  fnasrng  5375  fpr  5377  fmptap  5385  riotav  5504  dmoprab  5616  rnoprab2  5619  mpt2v  5625  mpt2mptx  5626  abrexex2g  5778  abrexex2  5782  1stval2  5813  2ndval2  5814  fo1st  5815  fo2nd  5816  xp2  5830  dfoprab4f  5850  fmpt2co  5868  tposmpt2  5930  recsfval  5964  frecfnom  6050  freccllem  6051  frecfcllem  6053  frecsuclem  6055  df2o3  6078  o1p1e2  6112  ecqs  6234  qliftf  6257  erovlem  6264  xpf1o  6385  dmaddpq  6631  dmmulpq  6632  enq0enq  6683  nqprlu  6799  m1p1sr  6999  m1m1sr  7000  caucvgsr  7040  dfcnqs  7071  3m1e2  8225  2p2e4  8226  3p2e5  8240  3p3e6  8241  4p2e6  8242  4p3e7  8243  4p4e8  8244  5p2e7  8245  5p3e8  8246  5p4e9  8247  6p2e8  8248  6p3e9  8249  7p2e9  8250  nn0supp  8407  nnzrab  8456  nn0zrab  8457  dec0u  8578  dec0h  8579  decsuc  8588  decsucc  8598  numma  8601  decma  8608  decmac  8609  decma2c  8610  decadd  8611  decaddc  8612  decmul1  8621  decmul1c  8622  decmul2c  8623  5p5e10  8628  6p4e10  8629  7p3e10  8632  8p2e10  8637  5t5e25  8660  6t6e36  8665  8t6e48  8676  nn0uz  8734  nnuz  8735  ioomax  9047  iccmax  9048  ioopos  9049  ioorp  9050  fseq1p1m1  9187  fzo0to2pr  9304  fzo0to3tp  9305  frecfzennn  9508  irec  9671  sq10e99m1  9738  facnn  9751  fac0  9752  faclbnd2  9766  minmax  10250  unennn  10708  bj-omind  10887
  Copyright terms: Public domain W3C validator