New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > 3eqtr4ri | Unicode version |
Description: An inference from three chained equalities. (Contributed by NM, 2-Sep-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
Ref | Expression |
---|---|
3eqtr4i.1 | |
3eqtr4i.2 | |
3eqtr4i.3 |
Ref | Expression |
---|---|
3eqtr4ri |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3eqtr4i.3 | . . 3 | |
2 | 3eqtr4i.1 | . . 3 | |
3 | 1, 2 | eqtr4i 2376 | . 2 |
4 | 3eqtr4i.2 | . 2 | |
5 | 3, 4 | eqtr4i 2376 | 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: cbvreucsf 3200 dfin3 3494 dfin5 3545 dfif6 3665 qdass 3819 tpidm12 3821 ssfin 4470 nnadjoin 4520 nulnnn 4556 df1st2 4738 dfsset2 4743 dfco1 4748 dfsi2 4751 resres 4980 inres 4985 cnvun 5033 coundi 5082 coundir 5083 snec 5987 df0c2 6137 1cnc 6139 1p1e2c 6155 2p1e3c 6156 |
Copyright terms: Public domain | W3C validator |