![]() |
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 2467 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | eqeq12i.2 |
. . 3
![]() ![]() ![]() ![]() | |
4 | 3 | eqeq2i 2474 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2, 4 | bitri 257 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1680 ax-4 1693 ax-ext 2442 |
This theorem depends on definitions: df-bi 190 df-cleq 2455 |
This theorem is referenced by: neeq12i 2702 rabbi 2981 unineq 3705 sbceqg 3785 rabeqsn 4013 preq2b 4160 preqr2 4163 iuneq12df 4316 otth 4701 otthg 4702 rncoeq 5120 sspred 5411 fresaunres1 5783 eqfnov 6434 mpt22eqb 6437 f1o2ndf1 6936 wfrlem5 7071 ecopovsym 7496 karden 8397 adderpqlem 9410 mulerpqlem 9411 addcmpblnr 9524 ax1ne0 9615 addid1 9844 sq11i 12403 nn0opth2i 12495 oppgcntz 17070 islpir 18528 evlsval 18797 volfiniun 22556 dvmptfsum 22983 axlowdimlem13 25040 usgraidx2v 25176 el2wlkonotot0 25656 pjneli 27432 iuneq12daf 28225 madjusmdetlem1 28704 bnj553 29759 bnj1253 29876 frrlem5 30568 sltval2 30593 sltsolem1 30607 altopthsn 30778 bj-2upleq 31652 relowlpssretop 31813 iscrngo2 32277 sbceqi 32394 cdleme18d 33907 fphpd 35705 rp-fakeuninass 36207 relexp0eq 36339 comptiunov2i 36344 onfrALTlem5 36953 onfrALTlem4 36954 onfrALTlem5VD 37323 onfrALTlem4VD 37324 dvnprodlem3 37909 sge0xadd 38380 usgredg2v 39450 issubgr 39489 usgedgvadf1 40096 usgedgvadf1ALT 40099 |
Copyright terms: Public domain | W3C validator |