![]() |
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 2210 | . 2 ⊢ (𝜑 → 𝐴 = 𝐶) |
4 | 3 | eqcomd 2183 | 1 ⊢ (𝜑 → 𝐶 = 𝐴) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1353 |
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 3574 ifordc 3575 onsucmin 4508 elxp4 5118 elxp5 5119 csbopeq1a 6191 ecinxp 6612 fundmen 6808 fidifsnen 6872 sbthlemi3 6960 ctm 7110 addpinq1 7465 1idsr 7769 prsradd 7787 cnegexlem3 8136 cnegex 8137 submul2 8358 mulsubfacd 8377 divadddivap 8686 infrenegsupex 9596 xadd4d 9887 fzval3 10206 fzoshftral 10240 ceiqm1l 10313 flqdiv 10323 flqmod 10340 intqfrac 10341 modqcyc2 10362 modqdi 10394 frecuzrdgtcl 10414 frecuzrdgfunlem 10421 seq3id2 10511 expnegzap 10556 binom2sub 10636 binom3 10640 fihashssdif 10800 reim 10863 mulreap 10875 addcj 10902 resqrexlemcalc1 11025 absimle 11095 infxrnegsupex 11273 clim2ser 11347 serf0 11362 summodclem3 11390 mptfzshft 11452 fsumrev 11453 fsum2mul 11463 isumsplit 11501 cvgratz 11542 mertenslemi1 11545 fprodrev 11629 ef4p 11704 tanval3ap 11724 efival 11742 sinmul 11754 divalglemnn 11925 dfgcd2 12017 lcmgcdlem 12079 lcm1 12083 oddpwdclemxy 12171 oddpwdclemdc 12175 eulerthlemth 12234 hashgcdeq 12241 powm2modprm 12254 pythagtriplem16 12281 pczpre 12299 pcqdiv 12309 pcadd 12341 pcfac 12350 4sqlem10 12387 ennnfonelemp1 12409 strslfvd 12506 xpsff1o 12773 grpinvssd 12952 grpinvval2 12958 opprringbg 13255 ringinvdv 13319 lss1d 13475 cnclima 13808 dveflem 14272 tangtx 14344 abssinper 14352 reexplog 14377 rprelogbdiv 14460 lgsdirnn0 14533 lgsdinn0 14534 lgseisenlem2 14536 2sqlem2 14547 mul2sq 14548 |
Copyright terms: Public domain | W3C validator |