![]() |
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 2124 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3eqtr4d.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | eqtr4d 2124 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1382 ax-gen 1384 ax-4 1446 ax-17 1465 ax-ext 2071 |
This theorem depends on definitions: df-bi 116 df-cleq 2082 |
This theorem is referenced by: csbcnvg 4635 fvco4 5391 phplem4 6627 phplem4on 6639 recexnq 7012 prarloclemcalc 7124 addcomprg 7200 mulcomprg 7202 mulcmpblnrlemg 7349 axmulass 7471 divnegap 8236 modqlt 9803 modqmulnn 9812 iseqvalt 9936 seq3val 9937 iseqcaopr3 9973 seq3f1olemqsumkj 9990 seq3f1olemqsumk 9991 seq3f1olemqsum 9992 seq3f1o 9996 ibcval5 10234 omgadd 10273 iseqcoll 10310 cjreb 10363 recj 10364 imcj 10372 imval2 10391 resqrexlemover 10506 sqrtmul 10531 amgm2 10614 maxabslemab 10702 isummolem2a 10834 fsumf1o 10845 sumsnf 10866 sumsplitdc 10889 fsummulc2 10905 binom 10941 bcxmas 10946 expcnvap0 10959 expcnv 10961 cvgratnnlemnexp 10981 cvgratnnlemmn 10982 ege2le3 11024 efaddlem 11027 eftlub 11043 tanval3ap 11068 tannegap 11082 cosmul 11099 cos01bnd 11112 demoivreALT 11126 flodddiv4 11275 dfgcd3 11340 absmulgcd 11347 sqpweven 11494 2sqpwodd 11495 crth 11541 setsslnid 11608 |
Copyright terms: Public domain | W3C validator |