![]() |
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 | eqtrid 2777 | . 2 ⊢ (𝜑 → 𝐴 = 𝐷) |
5 | 1, 4 | eqtr3d 2767 | 1 ⊢ (𝜑 → 𝐶 = 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1533 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-9 2108 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1774 df-cleq 2717 |
This theorem is referenced by: uneqin 4277 coi2 6269 foima 6815 f1imacnv 6854 fvsnun1 7191 fnsnsplit 7193 phplem2 9233 php3 9237 phplem4OLD 9245 php3OLD 9249 rankopb 9877 fin4en1 10334 fpwwe2 10668 winacard 10717 mul02lem1 11422 cnegex2 11428 crreczi 14226 hashinf 14330 hashcard 14350 cshw0 14780 cshwn 14783 sqrtneglem 15249 rlimresb 15545 bpoly3 16038 bpoly4 16039 sinhval 16134 coshval 16135 absefib 16178 efieq1re 16179 sadcaddlem 16435 sadaddlem 16444 qus0subgbas 19161 psgnsn 19487 odngen 19544 frlmup3 21751 mat0op 22365 restopnb 23123 cnmpt2t 23621 clmnegneg 25075 ncvspi 25128 volsup2 25578 plypf1 26191 pige3ALT 26499 sineq0 26503 eflog 26555 logef 26560 cxpsqrt 26682 dvcncxp1 26722 cubic2 26825 quart1 26833 asinsinlem 26868 asinsin 26869 2efiatan 26895 pclogsum 27193 lgsneg 27299 vc0 30456 vcm 30458 nvpi 30549 honegneg 31688 opsqrlem6 32027 sto1i 32118 mdexchi 32217 preiman0 32571 elrspunidl 33240 cnre2csqlem 33639 itgexpif 34366 subfacp1lem1 34917 rankaltopb 35703 poimirlem23 37244 dvtan 37271 dvasin 37305 heiborlem6 37417 trlcoat 40323 cdlemk54 40558 resubid 42095 sn-mul02 42127 iocunico 42778 relintab 43152 rfovcnvf1od 43573 ntrneifv3 43651 ntrneifv4 43654 clsneifv3 43679 clsneifv4 43680 neicvgfv 43690 snunioo1 45032 dvsinexp 45434 itgsubsticclem 45498 stirlinglem1 45597 fourierdlem80 45709 fourierdlem111 45740 sqwvfoura 45751 sqwvfourb 45752 fouriersw 45754 saliinclf 45849 smfco 46325 aacllem 48417 |
Copyright terms: Public domain | W3C validator |