![]() |
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 2780 | . 2 ⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐶) |
3 | eqeq12i.2 | . . 3 ⊢ 𝐶 = 𝐷 | |
4 | 3 | eqeq2i 2787 | . 2 ⊢ (𝐵 = 𝐶 ↔ 𝐵 = 𝐷) |
5 | 2, 4 | bitri 267 | 1 ⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 = wceq 1507 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1964 ax-9 2057 ax-ext 2747 |
This theorem depends on definitions: df-bi 199 df-an 388 df-ex 1743 df-cleq 2768 |
This theorem is referenced by: neeq12i 3030 rabbi 3319 unineq 4140 sbceqg 4245 sbceqi 4246 preq2b 4650 preqr2 4652 otth 5230 otthg 5231 rncoeq 5685 fresaunres1 6378 eqfnov 7094 mpo2eqb 7097 f1o2ndf1 7620 wfrlem5 7760 ecopovsym 8195 karden 9114 adderpqlem 10170 mulerpqlem 10171 addcmpblnr 10285 ax1ne0 10376 addid1 10616 sq11i 13366 nn0opth2i 13443 oppgcntz 18257 islpir 19737 evlsval 20006 volfiniun 23845 dvmptfsum 24269 axlowdimlem13 26437 usgredg2v 26706 issubgr 26750 clwlkcompbp 27265 pjneli 29275 madjusmdetlem1 30725 breprexp 31543 bnj553 31808 bnj1253 31925 fprlem1 32628 frrlem15 32633 sltval2 32654 sltsolem1 32671 nosepnelem 32675 nolt02o 32690 altopthsn 32913 bj-2upleq 33807 relowlpssretop 34052 iscrngo2 34695 extid 34990 cdleme18d 36854 fphpd 38787 rp-fakeuninass 39256 relexp0eq 39387 comptiunov2i 39392 clsk1indlem1 39736 ntrclskb 39760 onfrALTlem5 40272 onfrALTlem4 40273 onfrALTlem5VD 40615 onfrALTlem4VD 40616 dvnprodlem3 41642 sge0xadd 42127 reuabaiotaiota 42672 rrx2linest 44071 |
Copyright terms: Public domain | W3C validator |