Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3eqtr4ri | Structured version Visualization version 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 2647 | . 2 |
4 | 3eqtr4i.2 | . 2 | |
5 | 3, 4 | eqtr4i 2647 | 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: cbvreucsf 3567 dfin3 3866 dfsymdif3 3893 dfif6 4089 qdass 4288 tpidm12 4290 opid 4421 unipr 4449 iinvdif 4592 unidif0 4838 csbcnv 5306 dfdm4 5316 dmun 5331 resres 5409 inres 5414 resdifcom 5415 resiun1 5416 resiun1OLD 5417 imainrect 5575 cnvcnv 5586 coundi 5636 coundir 5637 funopg 5922 csbov 6688 elrnmpt2res 6774 offres 7163 1st2val 7194 2nd2val 7195 mpt2mptsx 7233 oeoalem 7676 omopthlem1 7735 snec 7810 tcsni 8619 infmap2 9040 ackbij2lem3 9063 itunisuc 9241 axmulass 9978 divmul13i 10786 dfnn3 11034 halfpm6th 11253 numsucc 11549 decbin2 11683 uzrdgxfr 12766 hashxplem 13220 prprrab 13255 ids1 13377 s3s4 13678 s2s5 13679 s5s2 13680 fsumadd 14470 fsum2d 14502 fprodmul 14690 bpoly3 14789 bezout 15260 ressbas 15930 oppchomf 16380 oppr1 18634 opsrtoslem1 19484 m2detleiblem2 20434 cnfldnm 22582 cnnm 22960 volres 23296 voliunlem1 23318 uniioombllem4 23354 itg11 23458 plyid 23965 coeidp 24019 dgrid 24020 dfrelog 24312 log2ublem3 24675 bposlem8 25016 uhgrspan1 26195 ip2i 27683 bcseqi 27977 hilnormi 28020 cmcmlem 28450 fh3i 28482 fh4i 28483 pjadjii 28533 cnvoprab 29498 resf1o 29505 dp3mul10 29606 dpmul4 29622 threehalves 29623 ressplusf 29650 resvsca 29830 xpinpreima 29952 cnre2csqima 29957 esum2dlem 30154 eulerpartgbij 30434 ballotth 30599 plymulx 30625 hgt750lem2 30730 elrn3 31652 domep 31698 itg2addnclem2 33462 areaquad 37802 cnvrcl0 37932 stoweidlem13 40230 wallispi2 40290 fourierdlem96 40419 fourierdlem97 40420 fourierdlem98 40421 fourierdlem99 40422 fourierdlem113 40436 fourierswlem 40447 dfnelbr2 41290 fmtnorec2 41455 fmtno5fac 41494 setrec2 42442 |
Copyright terms: Public domain | W3C validator |