New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > 3eqtr4i | Unicode version |
Description: An inference from three chained equalities. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
Ref | Expression |
---|---|
3eqtr4i.1 | |
3eqtr4i.2 | |
3eqtr4i.3 |
Ref | Expression |
---|---|
3eqtr4i |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3eqtr4i.2 | . 2 | |
2 | 3eqtr4i.3 | . . 3 | |
3 | 3eqtr4i.1 | . . 3 | |
4 | 2, 3 | eqtr4i 2376 | . 2 |
5 | 1, 4 | eqtr4i 2376 | 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: rabswap 2790 rabbiia 2849 cbvrab 2857 cbvcsb 3140 csbco 3145 cbvrabcsf 3201 un4 3423 in13 3468 in31 3469 in4 3471 indifcom 3500 indir 3503 undir 3504 notrab 3532 symdifcom 3542 dfnul3 3553 rab0 3571 dfif5 3674 prcom 3798 tprot 3815 tpcoma 3816 tpcomb 3817 tpass 3818 qdassr 3820 pwpw0 3855 pwsn 3881 pwsnALT 3882 int0 3940 cbviun 4003 cbviin 4004 iunrab 4013 iunin1 4031 pw0 4160 cbviota 4344 sb8iota 4346 addccom 4406 addc32 4416 nncaddccl 4419 ltfintrilem1 4465 phiun 4614 cbvopab 4630 cbvopab1 4632 cbvopab2 4633 cbvopab1s 4634 cbvopab2v 4636 unopab 4638 dfid3 4768 rabxp 4814 xpundi 4832 xpundir 4833 inxp 4863 cnvco 4894 resundi 4981 resundir 4982 resindi 4983 resindir 4984 rescom 4989 resima 5006 imadmrn 5008 cnvimarndm 5017 cnvi 5032 cnvin 5035 rnun 5036 imaundi 5039 cnvxp 5043 resdmres 5078 imadmres 5079 df2nd2 5111 iunfopab 5204 resdif 5306 fvco2 5382 fpr 5437 rnsi 5521 dfoprab2 5558 cbvoprab1 5567 cbvoprab2 5568 cbvoprab12 5569 cbvoprab3 5571 resoprab 5581 caov32 5635 caov31 5637 caov4 5639 caovlem2 5644 cbvmpt 5676 cbvmpt2x 5678 mptpreima 5682 fmpt2x 5730 cnvpprod 5841 rnpprod 5842 dfnnc3 5885 map0e 6023 enmap2lem1 6063 enmap1lem1 6069 muccom 6134 mucass 6135 muc0 6142 ncpw1c 6154 tce2 6236 addccan2nclem2 6264 nchoicelem1 6289 nchoicelem2 6290 nchoicelem16 6304 dmsnfn 6327 |
Copyright terms: Public domain | W3C validator |