Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3eqtr2ri | Structured version Visualization version Unicode version |
Description: An inference from three chained equalities. (Contributed by NM, 3-Aug-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
Ref | Expression |
---|---|
3eqtr2i.1 | |
3eqtr2i.2 | |
3eqtr2i.3 |
Ref | Expression |
---|---|
3eqtr2ri |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3eqtr2i.1 | . . 3 | |
2 | 3eqtr2i.2 | . . 3 | |
3 | 1, 2 | eqtr4i 2647 | . 2 |
4 | 3eqtr2i.3 | . 2 | |
5 | 3, 4 | eqtr2i 2645 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wceq 1483 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-an 386 df-ex 1705 df-cleq 2615 |
This theorem is referenced by: funimacnv 5970 uniqs 7807 ackbij1lem13 9054 ef01bndlem 14914 cos2bnd 14918 divalglem2 15118 decexp2 15779 lefld 17226 discmp 21201 unmbl 23305 sinhalfpilem 24215 log2cnv 24671 lgam1 24790 ip0i 27680 polid2i 28014 hh0v 28025 pjinormii 28535 dfdec100 29576 dpmul100 29605 dpmul 29621 dpmul4 29622 subfacp1lem3 31164 uniqsALTV 34101 cotrclrcl 38034 sqwvfoura 40445 sqwvfourb 40446 |
Copyright terms: Public domain | W3C validator |