![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eqtr2d | Unicode version |
Description: An equality transitivity deduction. (Contributed by NM, 18-Oct-1999.) |
Ref | Expression |
---|---|
eqtr2d.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
eqtr2d.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
eqtr2d |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqtr2d.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | eqtr2d.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | eqtrd 2120 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | eqcomd 2093 |
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: 3eqtrrd 2125 3eqtr2rd 2127 ifandc 3427 onsucmin 4324 elxp4 4918 elxp5 4919 csbopeq1a 5958 ecinxp 6367 fundmen 6523 fidifsnen 6586 sbthlemi3 6668 addpinq1 7023 1idsr 7314 prsradd 7331 cnegexlem3 7659 cnegex 7660 submul2 7877 mulsubfacd 7896 divadddivap 8194 infrenegsupex 9082 fzval3 9615 fzoshftral 9649 ceiqm1l 9718 flqdiv 9728 flqmod 9745 intqfrac 9746 modqcyc2 9767 modqdi 9799 frecuzrdgtcl 9819 frecuzrdgfunlem 9826 seq3id2 9940 iseqid2 9941 expnegzap 9989 binom2sub 10067 binom3 10071 fihashssdif 10226 reim 10286 mulreap 10298 addcj 10325 resqrexlemcalc1 10447 absimle 10517 clim2ser 10725 serf0 10741 isummolem3 10770 mptfzshft 10836 fsumrev 10837 fsum2mul 10847 isumsplit 10885 cvgratz 10926 mertenslemi1 10929 ef4p 10984 tanval3ap 11005 efival 11023 sinmul 11035 divalglemnn 11196 dfgcd2 11281 lcmgcdlem 11337 lcm1 11341 oddpwdclemxy 11425 oddpwdclemdc 11429 hashgcdeq 11482 strslfvd 11535 |
Copyright terms: Public domain | W3C validator |