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 276 | 1 ⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 = wceq 1528 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-9 2115 ax-ext 2793 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-cleq 2814 |
This theorem is referenced by: neeq12i 3082 rabbi 3384 unineq 4253 sbceqg 4360 sbceqi 4361 preq2b 4772 preqr2 4774 otth 5368 otthg 5369 rncoeq 5840 fresaunres1 6545 eqfnov 7269 mpo2eqb 7272 f1o2ndf1 7809 wfrlem5 7950 ecopovsym 8389 karden 9313 adderpqlem 10365 mulerpqlem 10366 addcmpblnr 10480 ax1ne0 10571 addid1 10809 sq11i 13544 nn0opth2i 13621 oppgcntz 18432 islpir 19952 evlsval 20229 volfiniun 24077 dvmptfsum 24501 axlowdimlem13 26668 usgredg2v 26937 issubgr 26981 clwlkcompbp 27491 pjneli 29428 madjusmdetlem1 30992 breprexp 31804 bnj553 32070 bnj1253 32187 gonanegoal 32497 goalrlem 32541 goalr 32542 fmlasucdisj 32544 satffunlem 32546 satffunlem1lem1 32547 satffunlem2lem1 32549 fprlem1 33035 frrlem15 33040 sltval2 33061 sltsolem1 33078 nosepnelem 33082 nolt02o 33097 altopthsn 33320 bj-2upleq 34222 relowlpssretop 34528 iscrngo2 35158 extid 35451 cdleme18d 37313 fphpd 39293 rp-fakeuninass 39762 relexp0eq 39926 comptiunov2i 39931 clsk1indlem1 40275 ntrclskb 40299 onfrALTlem5 40756 onfrALTlem4 40757 onfrALTlem5VD 41099 onfrALTlem4VD 41100 dvnprodlem3 42113 sge0xadd 42598 reuabaiotaiota 43168 rrx2linest 44627 |
Copyright terms: Public domain | W3C validator |