Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > eqeq12i | Structured version Visualization version Unicode version |
Description: A useful inference for substituting definitions into an equality. (Contributed by NM, 15-Jul-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 20-Nov-2019.) |
Ref | Expression |
---|---|
eqeq12i.1 | |
eqeq12i.2 |
Ref | Expression |
---|---|
eqeq12i |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqeq12i.1 | . . 3 | |
2 | 1 | eqeq1i 2627 | . 2 |
3 | eqeq12i.2 | . . 3 | |
4 | 3 | eqeq2i 2634 | . 2 |
5 | 2, 4 | bitri 264 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wb 196 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: neeq12i 2860 rabbi 3120 unineq 3877 sbceqg 3984 rabeqsn 4214 preq2b 4378 preqr2 4381 iuneq12df 4544 otth 4953 otthg 4954 rncoeq 5389 fresaunres1 6077 eqfnov 6766 mpt22eqb 6769 f1o2ndf1 7285 wfrlem5 7419 ecopovsym 7849 karden 8758 adderpqlem 9776 mulerpqlem 9777 addcmpblnr 9890 ax1ne0 9981 addid1 10216 sq11i 12954 nn0opth2i 13058 oppgcntz 17794 islpir 19249 evlsval 19519 volfiniun 23315 dvmptfsum 23738 axlowdimlem13 25834 usgredg2v 26119 issubgr 26163 pjneli 28582 iuneq12daf 29373 madjusmdetlem1 29893 breprexp 30711 bnj553 30968 bnj1253 31085 frrlem5 31784 sltval2 31809 sltsolem1 31826 nosepnelem 31830 nolt02o 31845 altopthsn 32068 bj-2upleq 33000 relowlpssretop 33212 iscrngo2 33796 sbceqi 33913 extid 34081 cdleme18d 35582 fphpd 37380 rp-fakeuninass 37862 relexp0eq 37993 comptiunov2i 37998 clsk1indlem1 38343 ntrclskb 38367 onfrALTlem5 38757 onfrALTlem4 38758 onfrALTlem5VD 39121 onfrALTlem4VD 39122 dvnprodlem3 40163 sge0xadd 40652 |
Copyright terms: Public domain | W3C validator |