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 2656 | . 2 ⊢ (𝜑 → 𝐴 = 𝐷) |
5 | 1, 4 | eqtr3d 2646 | 1 ⊢ (𝜑 → 𝐶 = 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1475 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-cleq 2603 |
This theorem is referenced by: uneqin 3837 coi2 5569 foima 6033 f1imacnv 6066 fvsnun2 6354 fnsnsplit 6355 phplem4 8027 php3 8031 rankopb 8598 fin4en1 9014 fpwwe2 9344 winacard 9393 mul02lem1 10091 cnegex2 10097 crreczi 12851 hashinf 12984 hashcard 13008 cshw0 13391 cshwn 13394 sqrtneglem 13855 rlimresb 14144 bpoly3 14628 bpoly4 14629 sinhval 14723 coshval 14724 absefib 14767 efieq1re 14768 sadcaddlem 15017 sadaddlem 15026 psgnsn 17763 odngen 17815 frlmup3 19958 mat0op 20044 restopnb 20789 cnmpt2t 21286 clmnegneg 22712 ncvspi 22764 volsup2 23179 plypf1 23772 pige3 24073 sineq0 24077 eflog 24127 logef 24132 cxpsqrt 24249 dvcncxp1 24284 cubic2 24375 quart1 24383 asinsinlem 24418 asinsin 24419 2efiatan 24445 pclogsum 24740 lgsneg 24846 numclwlk1lem2fo 26622 vc0 26813 vcm 26815 nvpi 26906 honegneg 28049 opsqrlem6 28388 sto1i 28479 mdexchi 28578 cnre2csqlem 29284 subfacp1lem1 30415 rankaltopb 31256 poimirlem23 32602 dvtan 32630 dvasin 32666 heiborlem6 32785 trlcoat 35029 cdlemk54 35264 iocunico 36815 relintab 36908 rfovcnvf1od 37318 ntrneifv3 37400 ntrneifv4 37403 clsneifv3 37428 clsneifv4 37429 neicvgfv 37439 snunioo1 38585 dvsinexp 38798 itgsubsticclem 38867 stirlinglem1 38967 fourierdlem80 39079 fourierdlem111 39110 sqwvfoura 39121 sqwvfourb 39122 fouriersw 39124 av-numclwlk1lem2fo 41525 aacllem 42356 |
Copyright terms: Public domain | W3C validator |