![]() |
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 2099 | . 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐶) | |
4 | 1, 2, 3 | syl2an 283 | 1 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 = 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: sylan9req 2135 sylan9eqr 2136 difeq12 3086 uneq12 3122 ineq12 3163 ifeq12 3367 preq12 3473 prprc 3504 preq12b 3564 opeq12 3574 xpeq12 4384 nfimad 4701 coi2 4861 funimass1 5001 f1orescnv 5167 resdif 5173 oveq12 5546 cbvmpt2v 5609 ovmpt2g 5660 eqopi 5823 fmpt2co 5862 nnaordex 6159 xpcomco 6360 phplem3 6379 phplem4 6380 addcmpblnq 6608 ltrnqg 6661 enq0ref 6674 addcmpblnq0 6684 distrlem4prl 6825 distrlem4pru 6826 recexgt0sr 7001 axcnre 7098 cnegexlem2 7340 cnegexlem3 7341 recexap 7799 frec2uzrand 9476 iseqeq3 9515 shftcan1 9849 remul2 9887 immul2 9894 dvdsnegb 10346 dvdscmul 10356 dvds2ln 10362 dvds2add 10363 dvds2sub 10364 gcdn0val 10486 rpmulgcd 10548 lcmval 10578 lcmn0val 10581 |
Copyright terms: Public domain | W3C validator |