New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > 3eqtri | Unicode version |
Description: An inference from three chained equalities. (Contributed by NM, 29-Aug-1993.) |
Ref | Expression |
---|---|
3eqtri.1 | |
3eqtri.2 | |
3eqtri.3 |
Ref | Expression |
---|---|
3eqtri |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3eqtri.1 | . 2 | |
2 | 3eqtri.2 | . . 3 | |
3 | 3eqtri.3 | . . 3 | |
4 | 2, 3 | eqtri 2373 | . 2 |
5 | 1, 4 | eqtri 2373 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wceq 1642 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 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: csbid 3143 un23 3422 in32 3467 dfrab2 3530 undifv 3624 undif2 3626 undifabs 3627 difun2 3629 difdifdir 3637 dfif4 3673 tpidm23 3823 unisn 3907 incompl 4073 pw10 4161 xpun 4834 dfdmf 4905 dfrnf 4962 res0 4977 resres 4980 resopab 4999 imai 5010 ima0 5013 epini 5021 imaundir 5040 dmtpop 5071 resdmres 5078 dmco 5089 coi2 5095 fvsnun1 5447 fvsnun2 5448 dmoprab 5574 rnoprab 5576 ov6g 5600 dmmpt 5683 rnmpt2 5717 cnvpprod 5841 mucid1 6143 sbthlem1 6203 scancan 6331 |
Copyright terms: Public domain | W3C validator |