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 2157 | . 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐶) | |
4 | 1, 2, 3 | syl2an 287 | 1 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 = wceq 1331 |
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 1423 ax-gen 1425 ax-4 1487 ax-17 1506 ax-ext 2121 |
This theorem depends on definitions: df-bi 116 df-cleq 2132 |
This theorem is referenced by: sylan9req 2193 sylan9eqr 2194 difeq12 3189 uneq12 3225 ineq12 3272 ifeq12 3488 preq12 3602 prprc 3633 preq12b 3697 opeq12 3707 xpeq12 4558 nfimad 4890 coi2 5055 funimass1 5200 f1orescnv 5383 resdif 5389 oveq12 5783 cbvmpov 5851 ovmpog 5905 eqopi 6070 fmpoco 6113 nnaordex 6423 map0g 6582 xpcomco 6720 xpmapenlem 6743 phplem3 6748 phplem4 6749 sbthlemi5 6849 addcmpblnq 7175 ltrnqg 7228 enq0ref 7241 addcmpblnq0 7251 distrlem4prl 7392 distrlem4pru 7393 recexgt0sr 7581 axcnre 7689 cnegexlem2 7938 cnegexlem3 7939 recexap 8414 xaddpnf2 9630 xaddmnf2 9632 rexadd 9635 xaddnemnf 9640 xaddnepnf 9641 xposdif 9665 frec2uzrand 10178 seqeq3 10223 shftcan1 10606 remul2 10645 immul2 10652 ef0lem 11366 efieq1re 11478 dvdsnegb 11510 dvdscmul 11520 dvds2ln 11526 dvds2add 11527 dvds2sub 11528 gcdn0val 11650 rpmulgcd 11714 lcmval 11744 lcmn0val 11747 isopn3 12294 dvexp 12844 dvexp2 12845 subctctexmid 13196 |
Copyright terms: Public domain | W3C validator |