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 2615 | . 2 ⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐶) |
3 | eqeq12i.2 | . . 3 ⊢ 𝐶 = 𝐷 | |
4 | 3 | eqeq2i 2622 | . 2 ⊢ (𝐵 = 𝐶 ↔ 𝐵 = 𝐷) |
5 | 2, 4 | bitri 263 | 1 ⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 = wceq 1475 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-cleq 2603 |
This theorem is referenced by: neeq12i 2848 rabbi 3097 unineq 3836 sbceqg 3936 rabeqsn 4161 preq2b 4318 preqr2 4321 iuneq12df 4480 otth 4879 otthg 4880 rncoeq 5310 fresaunres1 5990 eqfnov 6664 mpt22eqb 6667 f1o2ndf1 7172 wfrlem5 7306 ecopovsym 7736 karden 8641 adderpqlem 9655 mulerpqlem 9656 addcmpblnr 9769 ax1ne0 9860 addid1 10095 sq11i 12816 nn0opth2i 12920 oppgcntz 17617 islpir 19070 evlsval 19340 volfiniun 23122 dvmptfsum 23542 axlowdimlem13 25634 usgraidx2v 25922 el2wlkonotot0 26399 pjneli 27966 iuneq12daf 28756 madjusmdetlem1 29221 bnj553 30222 bnj1253 30339 frrlem5 31028 sltval2 31053 sltsolem1 31067 altopthsn 31238 bj-2upleq 32193 relowlpssretop 32388 iscrngo2 32966 sbceqi 33083 cdleme18d 34600 fphpd 36398 rp-fakeuninass 36881 relexp0eq 37012 comptiunov2i 37017 clsk1indlem1 37363 ntrclskb 37387 onfrALTlem5 37778 onfrALTlem4 37779 onfrALTlem5VD 38143 onfrALTlem4VD 38144 dvnprodlem3 38838 sge0xadd 39328 usgredg2v 40454 issubgr 40495 |
Copyright terms: Public domain | W3C validator |