![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3eqtr3rd | Unicode version |
Description: A deduction from three chained equalities. (Contributed by NM, 14-Jan-2006.) |
Ref | Expression |
---|---|
3eqtr3d.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3eqtr3d.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3eqtr3d.3 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
3eqtr3rd |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3eqtr3d.3 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 3eqtr3d.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 3eqtr3d.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | eqtr3d 2122 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | eqtr3d 2122 |
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 104 ax-ia2 105 ax-ia3 106 ax-5 1381 ax-gen 1383 ax-4 1445 ax-17 1464 ax-ext 2070 |
This theorem depends on definitions: df-bi 115 df-cleq 2081 |
This theorem is referenced by: fcofo 5563 fcof1o 5568 frecabcl 6164 nnaword 6268 enomnilem 6792 fodjuomnilem0 6800 pn0sr 7315 negeu 7671 add20 7950 2halves 8643 bcnn 10161 bcpasc 10170 resqrexlemover 10439 fsumneg 10841 geolim 10901 geolim2 10902 mertensabs 10927 sincossq 11035 demoivre 11058 eirraplem 11060 gcdid 11251 phiprmpw 11472 |
Copyright terms: Public domain | W3C validator |