![]() |
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 3007 rabbi 3431 unineq 4241 vn0 4302 sbceqg 4373 sbceqi 4374 preq2b 4809 preqr2 4811 otth 5445 otthg 5446 rncoeq 5934 fresaunres1 6719 eqfnov 7489 mpo2eqb 7492 f1o2ndf1 8058 fprlem1 8235 wfrlem5OLD 8263 ecopovsym 8764 frrlem15 9701 karden 9839 adderpqlem 10898 mulerpqlem 10899 addcmpblnr 11013 ax1ne0 11104 addrid 11343 sq11i 14104 nn0opth2i 14180 oppgcntz 19153 islpir 20764 evlsval 21519 volfiniun 24934 dvmptfsum 25362 sltval2 27027 sltsolem1 27046 nosepnelem 27050 nolt02o 27066 axlowdimlem13 27952 usgredg2v 28224 issubgr 28268 clwlkcompbp 28779 pjneli 30714 indifbi 31497 madjusmdetlem1 32472 breprexp 33310 bnj553 33574 bnj1253 33693 gonanegoal 34010 goalrlem 34054 goalr 34055 fmlasucdisj 34057 satffunlem 34059 satffunlem1lem1 34060 satffunlem2lem1 34062 altopthsn 34599 bj-2upleq 35533 relowlpssretop 35885 iscrngo2 36506 extid 36821 cdleme18d 38808 fphpd 41186 oenassex 41700 rp-fakeuninass 41880 relexp0eq 42065 comptiunov2i 42070 clsk1indlem1 42409 ntrclskb 42433 onfrALTlem5 42916 onfrALTlem4 42917 onfrALTlem5VD 43259 onfrALTlem4VD 43260 dvnprodlem3 44279 sge0xadd 44766 reuabaiotaiota 45409 rrx2linest 46918 |
Copyright terms: Public domain | W3C validator |