![]() |
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 2114 | . 2 ⊢ (𝜑 → 𝐴 = 𝐶) |
4 | 3 | eqcomd 2087 | 1 ⊢ (𝜑 → 𝐶 = 𝐴) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1285 |
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 1377 ax-gen 1379 ax-4 1441 ax-17 1460 ax-ext 2064 |
This theorem depends on definitions: df-bi 115 df-cleq 2075 |
This theorem is referenced by: 3eqtrrd 2119 3eqtr2rd 2121 onsucmin 4259 elxp4 4838 elxp5 4839 csbopeq1a 5845 ecinxp 6247 fundmen 6353 fidifsnen 6405 addpinq1 6716 1idsr 7007 prsradd 7024 cnegexlem3 7352 cnegex 7353 submul2 7570 mulsubfacd 7589 divadddivap 7882 infrenegsupex 8763 fzval3 9290 fzoshftral 9324 ceiqm1l 9393 flqdiv 9403 flqmod 9420 intqfrac 9421 modqcyc2 9442 modqdi 9474 frecuzrdgtcl 9494 frecuzrdgfunlem 9501 iseqid2 9564 expnegzap 9607 binom2sub 9684 binom3 9687 reim 9877 mulreap 9889 addcj 9916 resqrexlemcalc1 10038 absimle 10108 clim2iser 10313 serif0 10327 divalglemnn 10462 dfgcd2 10547 lcmgcdlem 10603 lcm1 10607 oddpwdclemxy 10691 oddpwdclemdc 10695 |
Copyright terms: Public domain | W3C validator |