![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3eqtr4rd | GIF version |
Description: A deduction from three chained equalities. (Contributed by NM, 21-Sep-1995.) |
Ref | Expression |
---|---|
3eqtr4d.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
3eqtr4d.2 | ⊢ (𝜑 → 𝐶 = 𝐴) |
3eqtr4d.3 | ⊢ (𝜑 → 𝐷 = 𝐵) |
Ref | Expression |
---|---|
3eqtr4rd | ⊢ (𝜑 → 𝐷 = 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3eqtr4d.3 | . . 3 ⊢ (𝜑 → 𝐷 = 𝐵) | |
2 | 3eqtr4d.1 | . . 3 ⊢ (𝜑 → 𝐴 = 𝐵) | |
3 | 1, 2 | eqtr4d 2118 | . 2 ⊢ (𝜑 → 𝐷 = 𝐴) |
4 | 3eqtr4d.2 | . 2 ⊢ (𝜑 → 𝐶 = 𝐴) | |
5 | 3, 4 | eqtr4d 2118 | 1 ⊢ (𝜑 → 𝐷 = 𝐶) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = 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 2065 |
This theorem depends on definitions: df-bi 115 df-cleq 2076 |
This theorem is referenced by: csbcnvg 4567 phplem4 6411 phplem4on 6423 recexnq 6694 prarloclemcalc 6806 addcomprg 6882 mulcomprg 6884 mulcmpblnrlemg 7031 axmulass 7153 divnegap 7913 modqlt 9467 modqmulnn 9476 iseqvalt 9584 iseqcaopr3 9608 ibcval5 9839 omgadd 9878 cjreb 9954 recj 9955 imcj 9963 imval2 9982 resqrexlemover 10097 sqrtmul 10122 amgm2 10205 maxabslemab 10293 flodddiv4 10541 dfgcd3 10606 absmulgcd 10613 sqpweven 10760 2sqpwodd 10761 crth 10807 |
Copyright terms: Public domain | W3C validator |