Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 3eqtr4rd | Unicode version |
Description: A deduction from three chained equalities. (Contributed by NM, 21-Sep-1995.) |
Ref | Expression |
---|---|
3eqtr4d.1 | |
3eqtr4d.2 | |
3eqtr4d.3 |
Ref | Expression |
---|---|
3eqtr4rd |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3eqtr4d.3 | . . 3 | |
2 | 3eqtr4d.1 | . . 3 | |
3 | 1, 2 | eqtr4d 2175 | . 2 |
4 | 3eqtr4d.2 | . 2 | |
5 | 3, 4 | eqtr4d 2175 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wceq 1331 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1423 ax-gen 1425 ax-4 1487 ax-17 1506 ax-ext 2121 |
This theorem depends on definitions: df-bi 116 df-cleq 2132 |
This theorem is referenced by: csbcnvg 4723 fvco4 5493 phplem4 6749 phplem4on 6761 omp1eomlem 6979 ctssdclemn0 6995 recexnq 7198 prarloclemcalc 7310 addcomprg 7386 mulcomprg 7388 mulcmpblnrlemg 7548 axmulass 7681 divnegap 8466 modqlt 10106 modqmulnn 10115 seq3val 10231 seqvalcd 10232 seq3caopr3 10254 seq3f1olemqsumkj 10271 seq3f1olemqsumk 10272 seq3f1olemqsum 10273 seq3f1o 10277 bcval5 10509 omgadd 10548 seq3coll 10585 cjreb 10638 recj 10639 imcj 10647 imval2 10666 resqrexlemover 10782 sqrtmul 10807 amgm2 10890 maxabslemab 10978 xrmaxadd 11030 summodclem2a 11150 fsumf1o 11159 sumsnf 11178 sumsplitdc 11201 fsummulc2 11217 binom 11253 bcxmas 11258 expcnvap0 11271 expcnv 11273 cvgratnnlemnexp 11293 cvgratnnlemmn 11294 prodmodclem3 11344 ege2le3 11377 efaddlem 11380 eftlub 11396 tanval3ap 11421 tannegap 11435 cosmul 11452 cos01bnd 11465 demoivreALT 11480 flodddiv4 11631 dfgcd3 11698 absmulgcd 11705 sqpweven 11853 2sqpwodd 11854 crth 11900 ctiunctlemfo 11952 setsslnid 12010 txbasval 12436 |
Copyright terms: Public domain | W3C validator |