![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3eqtr3a | Structured version Visualization version GIF version |
Description: A chained equality inference, useful for converting from definitions. (Contributed by Mario Carneiro, 6-Nov-2015.) |
Ref | Expression |
---|---|
3eqtr3a.1 | ⊢ 𝐴 = 𝐵 |
3eqtr3a.2 | ⊢ (𝜑 → 𝐴 = 𝐶) |
3eqtr3a.3 | ⊢ (𝜑 → 𝐵 = 𝐷) |
Ref | Expression |
---|---|
3eqtr3a | ⊢ (𝜑 → 𝐶 = 𝐷) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3eqtr3a.2 | . 2 ⊢ (𝜑 → 𝐴 = 𝐶) | |
2 | 3eqtr3a.1 | . . 3 ⊢ 𝐴 = 𝐵 | |
3 | 3eqtr3a.3 | . . 3 ⊢ (𝜑 → 𝐵 = 𝐷) | |
4 | 2, 3 | syl5eq 2827 | . 2 ⊢ (𝜑 → 𝐴 = 𝐷) |
5 | 1, 4 | eqtr3d 2817 | 1 ⊢ (𝜑 → 𝐶 = 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1507 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-9 2059 ax-ext 2751 |
This theorem depends on definitions: df-bi 199 df-an 388 df-ex 1743 df-cleq 2772 |
This theorem is referenced by: uneqin 4143 coi2 5955 foima 6424 f1imacnv 6460 fvsnun1 6769 fvsnun2OLD 6772 fnsnsplit 6773 phplem4 8495 php3 8499 rankopb 9075 fin4en1 9529 fpwwe2 9863 winacard 9912 mul02lem1 10616 cnegex2 10622 crreczi 13404 hashinf 13510 hashcard 13531 cshw0 14018 cshwn 14021 sqrtneglem 14487 rlimresb 14783 bpoly3 15272 bpoly4 15273 sinhval 15367 coshval 15368 absefib 15411 efieq1re 15412 sadcaddlem 15666 sadaddlem 15675 psgnsn 18410 odngen 18463 frlmup3 20646 mat0op 20732 restopnb 21487 cnmpt2t 21985 clmnegneg 23411 ncvspi 23463 volsup2 23909 plypf1 24505 pige3ALT 24808 sineq0 24812 eflog 24861 logef 24866 cxpsqrt 24987 dvcncxp1 25025 cubic2 25127 quart1 25135 asinsinlem 25170 asinsin 25171 2efiatan 25197 pclogsum 25493 lgsneg 25599 vc0 28128 vcm 28130 nvpi 28221 honegneg 29364 opsqrlem6 29703 sto1i 29794 mdexchi 29893 cnre2csqlem 30794 itgexpif 31522 subfacp1lem1 32008 rankaltopb 32958 poimirlem23 34353 dvtan 34380 dvasin 34416 heiborlem6 34533 trlcoat 37301 cdlemk54 37536 iocunico 39210 relintab 39302 rfovcnvf1od 39710 ntrneifv3 39792 ntrneifv4 39795 clsneifv3 39820 clsneifv4 39821 neicvgfv 39831 snunioo1 41217 dvsinexp 41623 itgsubsticclem 41688 stirlinglem1 41788 fourierdlem80 41900 fourierdlem111 41931 sqwvfoura 41942 sqwvfourb 41943 fouriersw 41945 aacllem 44267 |
Copyright terms: Public domain | W3C validator |