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 2113 | . 2 ⊢ (𝜑 → 𝐴 = 𝐶) |
4 | 3 | eqcomd 2086 | 1 ⊢ (𝜑 → 𝐶 = 𝐴) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1284 |
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 1376 ax-gen 1378 ax-4 1440 ax-17 1459 ax-ext 2063 |
This theorem depends on definitions: df-bi 115 df-cleq 2074 |
This theorem is referenced by: 3eqtrrd 2118 3eqtr2rd 2120 onsucmin 4251 elxp4 4828 elxp5 4829 csbopeq1a 5834 ecinxp 6204 fundmen 6309 fidifsnen 6355 addpinq1 6654 1idsr 6945 prsradd 6962 cnegexlem3 7285 cnegex 7286 submul2 7503 mulsubfacd 7522 divadddivap 7815 infrenegsupex 8682 fzval3 9213 fzoshftral 9247 ceiqm1l 9313 flqdiv 9323 flqmod 9340 intqfrac 9341 modqcyc2 9362 modqdi 9394 frecuzrdgfn 9414 expnegzap 9510 binom2sub 9587 binom3 9590 reim 9739 mulreap 9751 addcj 9778 resqrexlemcalc1 9900 absimle 9970 clim2iser 10175 serif0 10189 divalglemnn 10318 dfgcd2 10403 lcmgcdlem 10459 lcm1 10463 oddpwdclemxy 10547 oddpwdclemdc 10551 |
Copyright terms: Public domain | W3C validator |