![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > eqeq12i | Structured version Visualization version GIF 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 2776 | . 2 ⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐶) |
3 | eqeq12i.2 | . . 3 ⊢ 𝐶 = 𝐷 | |
4 | 3 | eqeq2i 2783 | . 2 ⊢ (𝐵 = 𝐶 ↔ 𝐵 = 𝐷) |
5 | 2, 4 | bitri 264 | 1 ⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 = wceq 1631 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-9 2154 ax-ext 2751 |
This theorem depends on definitions: df-bi 197 df-an 383 df-ex 1853 df-cleq 2764 |
This theorem is referenced by: neeq12i 3009 rabbi 3269 unineq 4026 sbceqg 4129 rabeqsn 4353 preq2b 4511 preqr2 4513 iuneq12df 4679 otth 5081 otthg 5082 rncoeq 5526 fresaunres1 6218 eqfnov 6917 mpt22eqb 6920 f1o2ndf1 7440 wfrlem5 7576 ecopovsym 8006 karden 8926 adderpqlem 9982 mulerpqlem 9983 addcmpblnr 10096 ax1ne0 10187 addid1 10422 sq11i 13161 nn0opth2i 13262 oppgcntz 18001 islpir 19464 evlsval 19734 volfiniun 23535 dvmptfsum 23958 axlowdimlem13 26055 usgredg2v 26341 issubgr 26386 clwlkcompbp 26913 pjneli 28922 iuneq12daf 29711 madjusmdetlem1 30233 breprexp 31051 bnj553 31306 bnj1253 31423 frrlem5 32121 sltval2 32146 sltsolem1 32163 nosepnelem 32167 nolt02o 32182 altopthsn 32405 bj-2upleq 33330 relowlpssretop 33548 iscrngo2 34126 sbceqi 34243 extid 34422 cdleme18d 36103 fphpd 37904 rp-fakeuninass 38386 relexp0eq 38517 comptiunov2i 38522 clsk1indlem1 38867 ntrclskb 38891 onfrALTlem5 39280 onfrALTlem4 39281 onfrALTlem5VD 39641 onfrALTlem4VD 39642 dvnprodlem3 40676 sge0xadd 41164 |
Copyright terms: Public domain | W3C validator |