Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 3eqtr3d | GIF version |
Description: A deduction from three chained equalities. (Contributed by NM, 4-Aug-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
Ref | Expression |
---|---|
3eqtr3d.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
3eqtr3d.2 | ⊢ (𝜑 → 𝐴 = 𝐶) |
3eqtr3d.3 | ⊢ (𝜑 → 𝐵 = 𝐷) |
Ref | Expression |
---|---|
3eqtr3d | ⊢ (𝜑 → 𝐶 = 𝐷) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3eqtr3d.1 | . . 3 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | 3eqtr3d.2 | . . 3 ⊢ (𝜑 → 𝐴 = 𝐶) | |
3 | 1, 2 | eqtr3d 2074 | . 2 ⊢ (𝜑 → 𝐵 = 𝐶) |
4 | 3eqtr3d.3 | . 2 ⊢ (𝜑 → 𝐵 = 𝐷) | |
5 | 3, 4 | eqtr3d 2074 | 1 ⊢ (𝜑 → 𝐶 = 𝐷) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1243 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1336 ax-gen 1338 ax-4 1400 ax-17 1419 ax-ext 2022 |
This theorem depends on definitions: df-bi 110 df-cleq 2033 |
This theorem is referenced by: mpteqb 5261 fvmptt 5262 fsnunfv 5363 f1ocnvfv1 5417 f1ocnvfv2 5418 fcof1 5423 caov12d 5682 caov13d 5684 caov411d 5686 caovimo 5694 grprinvlem 5695 grprinvd 5696 grpridd 5697 tfrlem5 5930 tfrlemiubacc 5944 nndir 6069 fopwdom 6310 addassnqg 6480 distrnqg 6485 enq0tr 6532 distrnq0 6557 distnq0r 6561 addnqprl 6627 addnqpru 6628 appdivnq 6661 ltmprr 6740 addcmpblnr 6824 mulcmpblnrlemg 6825 ltsrprg 6832 1idsr 6853 pn0sr 6856 mulgt0sr 6862 axmulass 6947 ax0id 6952 recriota 6964 mul12 7142 mul4 7145 readdcan 7153 add12 7169 cnegexlem2 7187 addcan 7191 ppncan 7253 addsub4 7254 muladd 7381 mulcanapd 7642 receuap 7650 div13ap 7672 divdivdivap 7689 divcanap5 7690 divdivap1 7699 divdivap2 7700 halfaddsub 8159 fztp 8940 fseq1p1m1 8956 flqzadd 9140 flqdiv 9163 iseqm1 9227 iseqcaopr 9242 exprecap 9296 expsubap 9302 zesq 9367 shftval3 9428 crre 9457 resub 9470 imsub 9478 cjsub 9492 climshft2 9827 qdencn 10124 |
Copyright terms: Public domain | W3C validator |