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 2172 | . 2 ⊢ (𝜑 → 𝐴 = 𝐶) |
4 | 3 | eqcomd 2145 | 1 ⊢ (𝜑 → 𝐶 = 𝐴) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1331 |
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 1423 ax-gen 1425 ax-4 1487 ax-17 1506 ax-ext 2121 |
This theorem depends on definitions: df-bi 116 df-cleq 2132 |
This theorem is referenced by: 3eqtrrd 2177 3eqtr2rd 2179 ifandc 3508 onsucmin 4423 elxp4 5026 elxp5 5027 csbopeq1a 6086 ecinxp 6504 fundmen 6700 fidifsnen 6764 sbthlemi3 6847 ctm 6994 addpinq1 7272 1idsr 7576 prsradd 7594 cnegexlem3 7939 cnegex 7940 submul2 8161 mulsubfacd 8180 divadddivap 8487 infrenegsupex 9389 xadd4d 9668 fzval3 9981 fzoshftral 10015 ceiqm1l 10084 flqdiv 10094 flqmod 10111 intqfrac 10112 modqcyc2 10133 modqdi 10165 frecuzrdgtcl 10185 frecuzrdgfunlem 10192 seq3id2 10282 expnegzap 10327 binom2sub 10405 binom3 10409 fihashssdif 10564 reim 10624 mulreap 10636 addcj 10663 resqrexlemcalc1 10786 absimle 10856 infxrnegsupex 11032 clim2ser 11106 serf0 11121 summodclem3 11149 mptfzshft 11211 fsumrev 11212 fsum2mul 11222 isumsplit 11260 cvgratz 11301 mertenslemi1 11304 ef4p 11400 tanval3ap 11421 efival 11439 sinmul 11451 divalglemnn 11615 dfgcd2 11702 lcmgcdlem 11758 lcm1 11762 oddpwdclemxy 11847 oddpwdclemdc 11851 hashgcdeq 11904 ennnfonelemp1 11919 strslfvd 12000 cnclima 12392 dveflem 12855 tangtx 12919 abssinper 12927 |
Copyright terms: Public domain | W3C validator |