![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eqtr2d | GIF 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 2132 | . 2 ⊢ (𝜑 → 𝐴 = 𝐶) |
4 | 3 | eqcomd 2105 | 1 ⊢ (𝜑 → 𝐶 = 𝐴) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1299 |
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 1391 ax-gen 1393 ax-4 1455 ax-17 1474 ax-ext 2082 |
This theorem depends on definitions: df-bi 116 df-cleq 2093 |
This theorem is referenced by: 3eqtrrd 2137 3eqtr2rd 2139 ifandc 3455 onsucmin 4361 elxp4 4962 elxp5 4963 csbopeq1a 6016 ecinxp 6434 fundmen 6630 fidifsnen 6693 sbthlemi3 6775 ctm 6909 addpinq1 7173 1idsr 7464 prsradd 7481 cnegexlem3 7810 cnegex 7811 submul2 8028 mulsubfacd 8047 divadddivap 8348 infrenegsupex 9239 xadd4d 9509 fzval3 9822 fzoshftral 9856 ceiqm1l 9925 flqdiv 9935 flqmod 9952 intqfrac 9953 modqcyc2 9974 modqdi 10006 frecuzrdgtcl 10026 frecuzrdgfunlem 10033 seq3id2 10123 expnegzap 10168 binom2sub 10246 binom3 10250 fihashssdif 10405 reim 10465 mulreap 10477 addcj 10504 resqrexlemcalc1 10626 absimle 10696 infxrnegsupex 10871 clim2ser 10945 serf0 10960 summodclem3 10988 mptfzshft 11050 fsumrev 11051 fsum2mul 11061 isumsplit 11099 cvgratz 11140 mertenslemi1 11143 ef4p 11198 tanval3ap 11219 efival 11237 sinmul 11249 divalglemnn 11410 dfgcd2 11495 lcmgcdlem 11551 lcm1 11555 oddpwdclemxy 11639 oddpwdclemdc 11643 hashgcdeq 11696 ennnfonelemp1 11711 strslfvd 11782 cnclima 12173 |
Copyright terms: Public domain | W3C validator |