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 2173 | . 2 ⊢ (𝜑 → 𝐷 = 𝐴) |
4 | 3eqtr4d.2 | . 2 ⊢ (𝜑 → 𝐶 = 𝐴) | |
5 | 3, 4 | eqtr4d 2173 | 1 ⊢ (𝜑 → 𝐷 = 𝐶) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = 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 2119 |
This theorem depends on definitions: df-bi 116 df-cleq 2130 |
This theorem is referenced by: csbcnvg 4718 fvco4 5486 phplem4 6742 phplem4on 6754 omp1eomlem 6972 ctssdclemn0 6988 recexnq 7191 prarloclemcalc 7303 addcomprg 7379 mulcomprg 7381 mulcmpblnrlemg 7541 axmulass 7674 divnegap 8459 modqlt 10099 modqmulnn 10108 seq3val 10224 seqvalcd 10225 seq3caopr3 10247 seq3f1olemqsumkj 10264 seq3f1olemqsumk 10265 seq3f1olemqsum 10266 seq3f1o 10270 bcval5 10502 omgadd 10541 seq3coll 10578 cjreb 10631 recj 10632 imcj 10640 imval2 10659 resqrexlemover 10775 sqrtmul 10800 amgm2 10883 maxabslemab 10971 xrmaxadd 11023 summodclem2a 11143 fsumf1o 11152 sumsnf 11171 sumsplitdc 11194 fsummulc2 11210 binom 11246 bcxmas 11251 expcnvap0 11264 expcnv 11266 cvgratnnlemnexp 11286 cvgratnnlemmn 11287 ege2le3 11366 efaddlem 11369 eftlub 11385 tanval3ap 11410 tannegap 11424 cosmul 11441 cos01bnd 11454 demoivreALT 11469 flodddiv4 11620 dfgcd3 11687 absmulgcd 11694 sqpweven 11842 2sqpwodd 11843 crth 11889 ctiunctlemfo 11941 setsslnid 11999 txbasval 12425 |
Copyright terms: Public domain | W3C validator |