Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > sylan9eq | GIF version |
Description: An equality transitivity deduction. (Contributed by NM, 8-May-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
Ref | Expression |
---|---|
sylan9eq.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
sylan9eq.2 | ⊢ (𝜓 → 𝐵 = 𝐶) |
Ref | Expression |
---|---|
sylan9eq | ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylan9eq.1 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | sylan9eq.2 | . 2 ⊢ (𝜓 → 𝐵 = 𝐶) | |
3 | eqtr 2188 | . 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐶) | |
4 | 1, 2, 3 | syl2an 287 | 1 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 = wceq 1348 |
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 1440 ax-gen 1442 ax-4 1503 ax-17 1519 ax-ext 2152 |
This theorem depends on definitions: df-bi 116 df-cleq 2163 |
This theorem is referenced by: sylan9req 2224 sylan9eqr 2225 difeq12 3240 uneq12 3276 ineq12 3323 ifeq12 3542 preq12 3662 prprc 3693 preq12b 3757 opeq12 3767 xpeq12 4630 nfimad 4962 coi2 5127 funimass1 5275 f1orescnv 5458 resdif 5464 oveq12 5862 cbvmpov 5933 ovmpog 5987 eqopi 6151 fmpoco 6195 nnaordex 6507 map0g 6666 xpcomco 6804 xpmapenlem 6827 phplem3 6832 phplem4 6833 sbthlemi5 6938 addcmpblnq 7329 ltrnqg 7382 enq0ref 7395 addcmpblnq0 7405 distrlem4prl 7546 distrlem4pru 7547 recexgt0sr 7735 axcnre 7843 cnegexlem2 8095 cnegexlem3 8096 recexap 8571 xaddpnf2 9804 xaddmnf2 9806 rexadd 9809 xaddnemnf 9814 xaddnepnf 9815 xposdif 9839 frec2uzrand 10361 seqeq3 10406 shftcan1 10798 remul2 10837 immul2 10844 fprodssdc 11553 ef0lem 11623 efieq1re 11734 dvdsnegb 11770 dvdscmul 11780 dvds2ln 11786 dvds2add 11787 dvds2sub 11788 gcdn0val 11916 rpmulgcd 11981 lcmval 12017 lcmn0val 12020 odzval 12195 pcmpt 12295 grpsubval 12749 isopn3 12919 dvexp 13469 dvexp2 13470 lgsval3 13713 lgsdinn0 13743 subctctexmid 14034 |
Copyright terms: Public domain | W3C validator |