![]() |
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 2195 | . 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐶) | |
4 | 1, 2, 3 | syl2an 289 | 1 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 = 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: sylan9req 2231 sylan9eqr 2232 difeq12 3250 uneq12 3286 ineq12 3333 ifeq12 3552 preq12 3673 prprc 3704 preq12b 3772 opeq12 3782 xpeq12 4647 nfimad 4981 coi2 5147 funimass1 5295 f1orescnv 5479 resdif 5485 oveq12 5886 cbvmpov 5957 ovmpog 6011 eqopi 6175 fmpoco 6219 nnaordex 6531 map0g 6690 xpcomco 6828 xpmapenlem 6851 phplem3 6856 phplem4 6857 sbthlemi5 6962 addcmpblnq 7368 ltrnqg 7421 enq0ref 7434 addcmpblnq0 7444 distrlem4prl 7585 distrlem4pru 7586 recexgt0sr 7774 axcnre 7882 cnegexlem2 8135 cnegexlem3 8136 recexap 8612 xaddpnf2 9849 xaddmnf2 9851 rexadd 9854 xaddnemnf 9859 xaddnepnf 9860 xposdif 9884 frec2uzrand 10407 seqeq3 10452 shftcan1 10845 remul2 10884 immul2 10891 fprodssdc 11600 ef0lem 11670 efieq1re 11781 dvdsnegb 11817 dvdscmul 11827 dvds2ln 11833 dvds2add 11834 dvds2sub 11835 gcdn0val 11964 rpmulgcd 12029 lcmval 12065 lcmn0val 12068 odzval 12243 pcmpt 12343 grpsubval 12924 crngpropd 13223 opprringbg 13255 dvdsrtr 13275 isopn3 13664 dvexp 14214 dvexp2 14215 lgsval3 14458 lgsdinn0 14488 subctctexmid 14789 |
Copyright terms: Public domain | W3C validator |