![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3eqtr2d | Unicode version |
Description: A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.) |
Ref | Expression |
---|---|
3eqtr2d.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3eqtr2d.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3eqtr2d.3 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
3eqtr2d |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3eqtr2d.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 3eqtr2d.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | eqtr4d 2124 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3eqtr2d.3 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | eqtrd 2121 |
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: fmptapd 5502 rdgisucinc 6164 mulidnq 7002 ltrnqg 7033 recexprlem1ssl 7246 recexprlem1ssu 7247 ltmprr 7255 mulcmpblnrlemg 7340 caucvgsrlemoffcau 7397 negsub 7784 neg2sub 7796 divmuleqap 8238 divneg2ap 8257 qapne 9178 binom2 10119 bcpasc 10228 crim 10346 remullem 10359 max0addsup 10706 isummolem2a 10825 isum1p 10940 geo2sum 10962 cvgratz 10980 efi4p 11062 tanaddap 11084 addcos 11091 cos2tsin 11096 demoivreALT 11117 omeo 11230 sqgcd 11350 |
Copyright terms: Public domain | W3C validator |