![]() |
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 2213 | . 2 ⊢ (𝜑 → 𝐷 = 𝐴) |
4 | 3eqtr4d.2 | . 2 ⊢ (𝜑 → 𝐶 = 𝐴) | |
5 | 3, 4 | eqtr4d 2213 | 1 ⊢ (𝜑 → 𝐷 = 𝐶) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = 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: csbcnvg 4811 fvco4 5588 phplem4 6854 phplem4on 6866 omp1eomlem 7092 ctssdclemn0 7108 recexnq 7388 prarloclemcalc 7500 addcomprg 7576 mulcomprg 7578 mulcmpblnrlemg 7738 axmulass 7871 divnegap 8661 modqlt 10330 modqmulnn 10339 seq3val 10455 seqvalcd 10456 seq3caopr3 10478 seq3f1olemqsumkj 10495 seq3f1olemqsumk 10496 seq3f1olemqsum 10497 seq3f1o 10501 bcval5 10738 omgadd 10777 seq3coll 10817 cjreb 10870 recj 10871 imcj 10879 imval2 10898 resqrexlemover 11014 sqrtmul 11039 amgm2 11122 maxabslemab 11210 xrmaxadd 11264 summodclem2a 11384 fsumf1o 11393 sumsnf 11412 sumsplitdc 11435 fsummulc2 11451 binom 11487 bcxmas 11492 expcnvap0 11505 expcnv 11507 cvgratnnlemnexp 11527 cvgratnnlemmn 11528 prodmodclem3 11578 fprodseq 11586 fprodf1o 11591 prodsnf 11595 fprodfac 11618 fprodabs 11619 ege2le3 11674 efaddlem 11677 eftlub 11693 tanval3ap 11717 tannegap 11731 cosmul 11748 cos01bnd 11761 demoivreALT 11776 flodddiv4 11933 dfgcd3 12005 absmulgcd 12012 sqpweven 12169 2sqpwodd 12170 crth 12218 eulerthlema 12224 phisum 12234 pythagtriplem14 12271 pythagtriplem19 12276 pcmul 12295 pcfac 12342 ctiunctlemfo 12434 setsslnid 12508 mulgnn0p1 12948 mulgneg 12955 mulgnn0dir 12966 srgpcomp 13126 opprring 13202 oppr1g 13205 invrfvald 13244 rdivmuldivd 13266 txbasval 13660 rplogbchbase 14261 lgsdir2 14327 lgsdir 14329 lgsdi 14331 lgsdirnn0 14341 lgsdinn0 14342 |
Copyright terms: Public domain | W3C validator |