![]() |
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 2130 | . 2 ⊢ (𝜑 → 𝐴 = 𝐶) |
4 | 3eqtr2d.3 | . 2 ⊢ (𝜑 → 𝐶 = 𝐷) | |
5 | 3, 4 | eqtrd 2127 | 1 ⊢ (𝜑 → 𝐴 = 𝐷) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1296 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1388 ax-gen 1390 ax-4 1452 ax-17 1471 ax-ext 2077 |
This theorem depends on definitions: df-bi 116 df-cleq 2088 |
This theorem is referenced by: fmptapd 5527 rdgisucinc 6188 ctm 6871 mulidnq 7045 ltrnqg 7076 recexprlem1ssl 7289 recexprlem1ssu 7290 ltmprr 7298 mulcmpblnrlemg 7383 caucvgsrlemoffcau 7440 negsub 7827 neg2sub 7839 divmuleqap 8281 divneg2ap 8300 qapne 9223 binom2 10180 bcpasc 10289 crim 10407 remullem 10420 max0addsup 10767 summodclem2a 10924 isum1p 11035 geo2sum 11057 cvgratz 11075 efi4p 11157 tanaddap 11179 addcos 11186 cos2tsin 11191 demoivreALT 11212 omeo 11325 sqgcd 11445 |
Copyright terms: Public domain | W3C validator |