![]() |
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 2210 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | eqcomd 2183 |
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 106 ax-ia2 107 ax-ia3 108 ax-5 1447 ax-gen 1449 ax-4 1510 ax-17 1526 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-cleq 2170 |
This theorem is referenced by: 3eqtrrd 2215 3eqtr2rd 2217 ifandc 3571 ifordc 3572 onsucmin 4503 elxp4 5112 elxp5 5113 csbopeq1a 6183 ecinxp 6604 fundmen 6800 fidifsnen 6864 sbthlemi3 6952 ctm 7102 addpinq1 7451 1idsr 7755 prsradd 7773 cnegexlem3 8121 cnegex 8122 submul2 8343 mulsubfacd 8362 divadddivap 8670 infrenegsupex 9580 xadd4d 9869 fzval3 10187 fzoshftral 10221 ceiqm1l 10294 flqdiv 10304 flqmod 10321 intqfrac 10322 modqcyc2 10343 modqdi 10375 frecuzrdgtcl 10395 frecuzrdgfunlem 10402 seq3id2 10492 expnegzap 10537 binom2sub 10616 binom3 10620 fihashssdif 10779 reim 10842 mulreap 10854 addcj 10881 resqrexlemcalc1 11004 absimle 11074 infxrnegsupex 11252 clim2ser 11326 serf0 11341 summodclem3 11369 mptfzshft 11431 fsumrev 11432 fsum2mul 11442 isumsplit 11480 cvgratz 11521 mertenslemi1 11524 fprodrev 11608 ef4p 11683 tanval3ap 11703 efival 11721 sinmul 11733 divalglemnn 11903 dfgcd2 11995 lcmgcdlem 12057 lcm1 12061 oddpwdclemxy 12149 oddpwdclemdc 12153 eulerthlemth 12212 hashgcdeq 12219 powm2modprm 12232 pythagtriplem16 12259 pczpre 12277 pcqdiv 12287 pcadd 12319 pcfac 12328 4sqlem10 12365 ennnfonelemp1 12387 strslfvd 12483 grpinvssd 12833 grpinvval2 12839 opprringbg 13072 ringinvdv 13134 cnclima 13383 dveflem 13847 tangtx 13919 abssinper 13927 reexplog 13952 rprelogbdiv 14035 lgsdirnn0 14108 lgsdinn0 14109 2sqlem2 14111 mul2sq 14112 |
Copyright terms: Public domain | W3C validator |