New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > eqtr4i | GIF version |
Description: An equality transitivity inference. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
eqtr4i.1 | ⊢ A = B |
eqtr4i.2 | ⊢ C = B |
Ref | Expression |
---|---|
eqtr4i | ⊢ A = C |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqtr4i.1 | . 2 ⊢ A = B | |
2 | eqtr4i.2 | . . 3 ⊢ C = B | |
3 | 2 | eqcomi 2357 | . 2 ⊢ B = C |
4 | 1, 3 | eqtri 2373 | 1 ⊢ A = C |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1642 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675 ax-11 1746 ax-ext 2334 |
This theorem depends on definitions: df-bi 177 df-ex 1542 df-cleq 2346 |
This theorem is referenced by: 3eqtr2i 2379 3eqtr2ri 2380 3eqtr4i 2383 3eqtr4ri 2384 rabab 2876 cbvralcsf 3198 cbvrabcsf 3201 dfdif2 3222 rabbi2dva 3463 uneqin 3506 unrab 3526 inrab 3527 inrab2 3528 difrab 3529 dfrab3ss 3533 rabun2 3534 rabxm 3573 difidALT 3619 difdifdir 3637 dfif3 3672 dfif5 3674 tpidm 3824 ssunpr 3868 sstp 3870 dfint2 3928 iunrab 4013 uniiun 4019 intiin 4020 0iin 4024 complV 4070 dfaddc2 4381 dfnnc2 4395 preaddccan2lem1 4454 ltfinex 4464 evenfinex 4503 oddfinex 4504 tfinnn 4534 spfinex 4537 dfop2 4575 dfproj12 4576 dfproj22 4577 phiall 4618 opeq 4619 dfima2 4745 xpundi 4832 xpundir 4833 dmun 4912 rnopab2 4968 resopab 4999 opabresid 5003 cnvun 5033 imaundir 5040 dmtpop 5071 rnco2 5088 dmco 5089 f1ococnv2 5309 dmoprab 5574 rnoprab2 5577 fnov 5591 fconstmpt 5681 dmmpt 5683 mpt2mptx 5708 mptv 5718 mpt2v 5719 dfswap3 5728 dfswap4 5729 releqmpt 5808 releqmpt2 5809 cupex 5816 composeex 5820 disjex 5823 addcfnex 5824 funsex 5828 fnsex 5832 crossex 5850 pw1fnex 5852 pw1fnf1o 5855 domfnex 5870 ranfnex 5871 transex 5910 refex 5911 antisymex 5912 connexex 5913 foundex 5914 extex 5915 symex 5916 qsexg 5982 ecqs 5988 enex 6031 enpw1pw 6075 enprmaplem1 6076 enprmaplem4 6079 mucex 6133 ncpw1c 6154 ceex 6174 ce0 6190 ce2 6192 leconnnc 6218 tcncv 6226 tce2 6236 tcfnex 6244 nmembers1lem1 6268 |
Copyright terms: Public domain | W3C validator |