Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > eqeqan12d | Structured version Visualization version Unicode version |
Description: A useful inference for substituting definitions into an equality. See also eqeqan12dALT 2639. (Contributed by NM, 9-Aug-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 20-Nov-2019.) |
Ref | Expression |
---|---|
eqeqan12d.1 | |
eqeqan12d.2 |
Ref | Expression |
---|---|
eqeqan12d |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqeqan12d.1 | . . 3 | |
2 | 1 | adantr 481 | . 2 |
3 | eqeqan12d.2 | . . 3 | |
4 | 3 | adantl 482 | . 2 |
5 | 2, 4 | eqeq12d 2637 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wb 196 wa 384 wceq 1483 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-an 386 df-ex 1705 df-cleq 2615 |
This theorem is referenced by: eqeqan12rd 2640 eqfnfv2 6312 f1mpt 6518 soisores 6577 xpopth 7207 f1o2ndf1 7285 fnwelem 7292 fnse 7294 tz7.48lem 7536 ecopoveq 7848 xpdom2 8055 unfilem2 8225 wemaplem1 8451 suc11reg 8516 oemapval 8580 cantnf 8590 wemapwe 8594 r0weon 8835 infxpen 8837 fodomacn 8879 sornom 9099 fin1a2lem2 9223 fin1a2lem4 9225 neg11 10332 subeqrev 10453 rpnnen1lem6 11819 rpnnen1OLD 11825 cnref1o 11827 xneg11 12046 injresinj 12589 modadd1 12707 modmul1 12723 modlteq 12744 sq11 12936 hashen 13135 fz1eqb 13145 eqwrd 13346 s111 13395 wrd2ind 13477 wwlktovf1 13700 cj11 13902 sqrt11 14003 sqabs 14047 recan 14076 reeff1 14850 efieq 14893 eulerthlem2 15487 vdwlem12 15696 xpsff1o 16228 ismhm 17337 gsmsymgreq 17852 symgfixf1 17857 odf1 17979 sylow1 18018 frgpuplem 18185 isdomn 19294 cygznlem3 19918 psgnghm 19926 tgtop11 20786 fclsval 21812 vitali 23382 recosf1o 24281 dvdsmulf1o 24920 fsumvma 24938 brcgr 25780 axlowdimlem15 25836 axcontlem1 25844 axcontlem4 25847 axcontlem7 25850 axcontlem8 25851 iswlk 26506 wlkpwwlkf1ouspgr 26765 wlknwwlksninj 26775 wlkwwlkinj 26782 wwlksnextinj 26794 clwwlksf1 26917 numclwlk1lem2f1 27227 grpoinvf 27386 hial2eq2 27964 bnj554 30969 erdszelem9 31181 mrsubff1 31411 msubff1 31453 mvhf1 31456 fneval 32347 topfneec2 32351 f1omptsnlem 33183 f1omptsn 33184 rdgeqoa 33218 poimirlem4 33413 poimirlem26 33435 poimirlem27 33436 ismtyval 33599 extep 34048 opideq 34110 wepwsolem 37612 fnwe2val 37619 aomclem8 37631 relexp0eq 37993 fmtnof1 41447 fmtnofac1 41482 prmdvdsfmtnof1 41499 sfprmdvdsmersenne 41520 isupwlk 41717 sprsymrelf1 41746 uspgrsprf1 41755 ismgmhm 41783 2zlidl 41934 |
Copyright terms: Public domain | W3C validator |