![]() |
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 2173 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | eqcomd 2146 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
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 1424 ax-gen 1426 ax-4 1488 ax-17 1507 ax-ext 2122 |
This theorem depends on definitions: df-bi 116 df-cleq 2133 |
This theorem is referenced by: 3eqtrrd 2178 3eqtr2rd 2180 ifandc 3513 onsucmin 4431 elxp4 5034 elxp5 5035 csbopeq1a 6094 ecinxp 6512 fundmen 6708 fidifsnen 6772 sbthlemi3 6855 ctm 7002 addpinq1 7296 1idsr 7600 prsradd 7618 cnegexlem3 7963 cnegex 7964 submul2 8185 mulsubfacd 8204 divadddivap 8511 infrenegsupex 9416 xadd4d 9698 fzval3 10012 fzoshftral 10046 ceiqm1l 10115 flqdiv 10125 flqmod 10142 intqfrac 10143 modqcyc2 10164 modqdi 10196 frecuzrdgtcl 10216 frecuzrdgfunlem 10223 seq3id2 10313 expnegzap 10358 binom2sub 10436 binom3 10440 fihashssdif 10596 reim 10656 mulreap 10668 addcj 10695 resqrexlemcalc1 10818 absimle 10888 infxrnegsupex 11064 clim2ser 11138 serf0 11153 summodclem3 11181 mptfzshft 11243 fsumrev 11244 fsum2mul 11254 isumsplit 11292 cvgratz 11333 mertenslemi1 11336 ef4p 11437 tanval3ap 11457 efival 11475 sinmul 11487 divalglemnn 11651 dfgcd2 11738 lcmgcdlem 11794 lcm1 11798 oddpwdclemxy 11883 oddpwdclemdc 11887 hashgcdeq 11940 ennnfonelemp1 11955 strslfvd 12039 cnclima 12431 dveflem 12895 tangtx 12967 abssinper 12975 reexplog 13000 rprelogbdiv 13082 |
Copyright terms: Public domain | W3C validator |