Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 3eqtr2d | GIF version |
Description: A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.) |
Ref | Expression |
---|---|
3eqtr2d.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
3eqtr2d.2 | ⊢ (𝜑 → 𝐶 = 𝐵) |
3eqtr2d.3 | ⊢ (𝜑 → 𝐶 = 𝐷) |
Ref | Expression |
---|---|
3eqtr2d | ⊢ (𝜑 → 𝐴 = 𝐷) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3eqtr2d.1 | . . 3 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | 3eqtr2d.2 | . . 3 ⊢ (𝜑 → 𝐶 = 𝐵) | |
3 | 1, 2 | eqtr4d 2075 | . 2 ⊢ (𝜑 → 𝐴 = 𝐶) |
4 | 3eqtr2d.3 | . 2 ⊢ (𝜑 → 𝐶 = 𝐷) | |
5 | 3, 4 | eqtrd 2072 | 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: fmptapd 5354 rdgisucinc 5972 mulidnq 6487 ltrnqg 6518 recexprlem1ssl 6731 recexprlem1ssu 6732 ltmprr 6740 mulcmpblnrlemg 6825 caucvgsrlemoffcau 6882 negsub 7259 neg2sub 7271 divmuleqap 7693 divneg2ap 7712 qapne 8574 binom2 9362 crim 9458 remullem 9471 |
Copyright terms: Public domain | W3C validator |