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 2826 | . 2 ⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐶) |
3 | eqeq12i.2 | . . 3 ⊢ 𝐶 = 𝐷 | |
4 | 3 | eqeq2i 2834 | . 2 ⊢ (𝐵 = 𝐶 ↔ 𝐵 = 𝐷) |
5 | 2, 4 | bitri 277 | 1 ⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 208 = wceq 1537 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-9 2124 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-ex 1781 df-cleq 2814 |
This theorem is referenced by: neeq12i 3082 rabbi 3383 unineq 4254 sbceqg 4361 sbceqi 4362 preq2b 4778 preqr2 4780 otth 5376 otthg 5377 rncoeq 5846 fresaunres1 6551 eqfnov 7280 mpo2eqb 7283 f1o2ndf1 7818 wfrlem5 7959 ecopovsym 8399 karden 9324 adderpqlem 10376 mulerpqlem 10377 addcmpblnr 10491 ax1ne0 10582 addid1 10820 sq11i 13555 nn0opth2i 13632 oppgcntz 18492 islpir 20022 evlsval 20299 volfiniun 24148 dvmptfsum 24572 axlowdimlem13 26740 usgredg2v 27009 issubgr 27053 clwlkcompbp 27563 pjneli 29500 madjusmdetlem1 31092 breprexp 31904 bnj553 32170 bnj1253 32289 gonanegoal 32599 goalrlem 32643 goalr 32644 fmlasucdisj 32646 satffunlem 32648 satffunlem1lem1 32649 satffunlem2lem1 32651 fprlem1 33137 frrlem15 33142 sltval2 33163 sltsolem1 33180 nosepnelem 33184 nolt02o 33199 altopthsn 33422 bj-2upleq 34327 relowlpssretop 34648 iscrngo2 35290 extid 35583 cdleme18d 37446 fphpd 39433 rp-fakeuninass 39902 relexp0eq 40066 comptiunov2i 40071 clsk1indlem1 40415 ntrclskb 40439 onfrALTlem5 40896 onfrALTlem4 40897 onfrALTlem5VD 41239 onfrALTlem4VD 41240 dvnprodlem3 42253 sge0xadd 42737 reuabaiotaiota 43307 rrx2linest 44749 |
Copyright terms: Public domain | W3C validator |