![]() |
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 2738 | . 2 ⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐶) |
3 | eqeq12i.2 | . . 3 ⊢ 𝐶 = 𝐷 | |
4 | 3 | eqeq2i 2746 | . 2 ⊢ (𝐵 = 𝐶 ↔ 𝐵 = 𝐷) |
5 | 2, 4 | bitri 275 | 1 ⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 = wceq 1542 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 df-cleq 2725 |
This theorem is referenced by: neeq12i 3008 rabbi 3463 unineq 4277 vn0 4338 sbceqg 4409 sbceqi 4410 preq2b 4848 preqr2 4850 otth 5484 otthg 5485 rncoeq 5973 fresaunres1 6762 eqfnov 7535 mpo2eqb 7538 f1o2ndf1 8105 fprlem1 8282 wfrlem5OLD 8310 ecopovsym 8810 frrlem15 9749 karden 9887 adderpqlem 10946 mulerpqlem 10947 addcmpblnr 11061 ax1ne0 11152 addrid 11391 sq11i 14152 nn0opth2i 14228 oppgcntz 19226 islpir 20880 evlsval 21641 volfiniun 25056 dvmptfsum 25484 sltval2 27149 sltsolem1 27168 nosepnelem 27172 nolt02o 27188 axlowdimlem13 28202 usgredg2v 28474 issubgr 28518 clwlkcompbp 29029 pjneli 30964 indifbi 31746 madjusmdetlem1 32796 breprexp 33634 bnj553 33898 bnj1253 34017 gonanegoal 34332 goalrlem 34376 goalr 34377 fmlasucdisj 34379 satffunlem 34381 satffunlem1lem1 34382 satffunlem2lem1 34384 altopthsn 34922 bj-2upleq 35882 relowlpssretop 36234 iscrngo2 36854 extid 37168 cdleme18d 39155 fphpd 41540 oenassex 42054 rp-fakeuninass 42253 relexp0eq 42438 comptiunov2i 42443 clsk1indlem1 42782 ntrclskb 42806 onfrALTlem5 43289 onfrALTlem4 43290 onfrALTlem5VD 43632 onfrALTlem4VD 43633 dvnprodlem3 44651 sge0xadd 45138 reuabaiotaiota 45782 rrx2linest 47382 |
Copyright terms: Public domain | W3C validator |