New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > eqtri | Unicode version |
Description: An equality transitivity inference. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
eqtri.1 | |
eqtri.2 |
Ref | Expression |
---|---|
eqtri |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqtri.1 | . 2 | |
2 | eqtri.2 | . . 3 | |
3 | 2 | eqeq2i 2363 | . 2 |
4 | 1, 3 | mpbi 199 | 1 |
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: eqtr2i 2374 eqtr3i 2375 eqtr4i 2376 3eqtri 2377 3eqtrri 2378 3eqtr2i 2379 cbvrab 2857 csb2 3138 cbvrabcsf 3201 difeq1 3246 difeq2 3247 symdifeq1 3248 symdifeq2 3249 difeq12i 3383 inrot 3470 dfun3 3493 dfin3 3494 invdif 3496 difundi 3507 difindi 3509 symdif1 3519 rabnc 3574 undif1 3625 ssdifin0 3631 dfif2 3664 dfif3 3672 dfif4 3673 dfif5 3674 ifbieq2i 3681 ifbieq12i 3683 pwjust 3723 snjust 3740 dfpr2 3749 difprsn1 3847 diftpsn3 3849 sspr 3869 sstp 3870 dfuni2 3893 intab 3956 intunsn 3965 rint0 3966 iunid 4021 viin 4025 iinrab 4028 iinrab2 4029 2iunin 4034 riin0 4039 uncompl 4074 inindif 4075 cokeq12i 4236 xpkexg 4288 pw1eqadj 4332 iotajust 4338 dfiota2 4340 dfiota4 4372 addcid1 4405 addcid2 4407 nnc0suc 4412 addc6 4418 nncaddccl 4419 nnsucelrlem3 4426 addcnnul 4453 ltfintr 4459 ltfintrilem1 4465 ncfinraise 4481 tfinnul 4491 tfinsuc 4498 tfin1c 4499 sucoddeven 4511 dfevenfin2 4512 dfoddfin2 4513 evenodddisj 4516 oddtfin 4518 nnadjoin 4520 sfindbl 4530 spfinex 4537 opeq12i 4583 phiun 4614 phialllem1 4616 phialllem2 4617 unopab 4638 dfid3 4768 elxpi 4800 csbxpg 4813 fconstopab 4815 inxp 4863 coeq12i 4880 dfrn3 4903 dmopab 4915 dmopab3 4917 dmxpin 4925 reseq12i 4932 dfima4 4952 rnopab 4967 rncoss 4972 rncoeq 4975 resundi 4981 resindi 4983 resopab 4999 resima2 5007 imadisj 5015 iniseg 5022 ndmima 5025 cnvin 5035 rnun 5036 imaundi 5039 cnvxp 5043 rnxp 5051 rnxpss 5053 dminxp 5061 dmpropg 5068 op1sta 5072 opswap 5074 op2nda 5076 resdmres 5078 coundi 5082 coundir 5083 funi 5137 funcnvuni 5161 funcnvres 5165 fnresdisj 5193 fv2 5324 dfimafn2 5367 fnimapr 5374 ressnop0 5436 fpr 5437 fvsnun1 5447 imauni 5465 rnsi 5521 resoprab 5581 ov 5595 ovigg 5596 ovg 5601 caov31 5637 caov42 5641 caovdilem 5643 caovmo 5645 cbvmpt 5676 mptpreima 5682 dmmpt 5683 dmmptss 5685 rnmpt 5686 mptfng 5688 fvmptg 5698 fvmpts 5701 fvmpt2i 5703 ovmpt4g 5710 ovmpt2x 5712 ovmpt2ga 5713 rnmpt2 5717 mptresid 5720 fvmptex 5721 f1od 5726 composefn 5818 cnvpprod 5841 rnpprod 5842 fvfullfun 5864 clos1conn 5879 clos1induct 5880 clos1basesuc 5882 dfec2 5948 ecidsn 5973 ecid 5989 pmvalg 6010 mapsn 6026 enadj 6060 nenpw1pwlem1 6084 mucnc 6131 mucass 6135 muc0 6142 1p1e2c 6155 2p1e3c 6156 tc2c 6166 fnce 6176 ce2 6192 ce2nc1 6193 ce2ncpw11c 6194 sbthlem1 6203 leconnnc 6218 tcfnex 6244 addcdi 6250 nmembers1lem1 6268 nmembers1 6271 nncdiv3 6277 nnc3n3p1 6278 nnc3n3p2 6279 nchoicelem2 6290 nchoicelem17 6305 frecexg 6312 dmfrec 6316 fnfreclem2 6318 fnfreclem3 6319 frec0 6321 frecsuc 6322 |
Copyright terms: Public domain | W3C validator |