![]() |
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 2223 | . 2 ⊢ (𝜑 → 𝐴 = 𝐶) |
4 | 3eqtr2d.3 | . 2 ⊢ (𝜑 → 𝐶 = 𝐷) | |
5 | 3, 4 | eqtrd 2220 | 1 ⊢ (𝜑 → 𝐴 = 𝐷) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1363 |
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 1457 ax-gen 1459 ax-4 1520 ax-17 1536 ax-ext 2169 |
This theorem depends on definitions: df-bi 117 df-cleq 2180 |
This theorem is referenced by: fmptapd 5720 rdgisucinc 6399 ctm 7121 mulidnq 7401 ltrnqg 7432 recexprlem1ssl 7645 recexprlem1ssu 7646 ltmprr 7654 mulcmpblnrlemg 7752 caucvgsrlemoffcau 7810 negsub 8218 neg2sub 8230 divmuleqap 8687 divneg2ap 8706 qapne 9652 seqvalcd 10472 binom2 10645 bcpasc 10759 crim 10880 remullem 10893 max0addsup 11241 summodclem2a 11402 isum1p 11513 geo2sum 11535 cvgratz 11553 efi4p 11738 tanaddap 11760 addcos 11767 cos2tsin 11772 demoivreALT 11794 omeo 11916 sqgcd 12043 eulerthlemth 12245 pythagtriplem16 12292 fldivp1 12359 pockthlem 12367 4sqlem10 12398 grpinvid2 12949 imasgrp2 13004 mulgaddcomlem 13037 mulgmodid 13053 ablsubsub 13154 ablsubsub4 13155 opprunitd 13353 lmodfopne 13510 txrest 14047 limccnpcntop 14415 dvrecap 14448 cosq34lt1 14542 lgseisenlem1 14721 |
Copyright terms: Public domain | W3C validator |