|   | 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 2741 | . 2 ⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐶) | 
| 3 | eqeq12i.2 | . . 3 ⊢ 𝐶 = 𝐷 | |
| 4 | 3 | eqeq2i 2749 | . 2 ⊢ (𝐵 = 𝐶 ↔ 𝐵 = 𝐷) | 
| 5 | 2, 4 | bitri 275 | 1 ⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐷) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ↔ wb 206 = wceq 1539 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1779 df-cleq 2728 | 
| This theorem is referenced by: neeq12i 3006 rabbi 3466 unineq 4287 vn0 4344 sbceqg 4411 sbceqi 4412 preq2b 4846 preqr2 4848 otth 5488 otthg 5489 rncoeq 5989 fresaunres1 6780 eqfnov 7563 mpo2eqb 7566 f1o2ndf1 8148 fprlem1 8326 wfrlem5OLD 8354 ecopovsym 8860 frrlem15 9798 karden 9936 adderpqlem 10995 mulerpqlem 10996 addcmpblnr 11110 ax1ne0 11201 addrid 11442 sq11i 14231 nn0opth2i 14311 oppgcntz 19384 opprdomnb 20718 isdomn4r 20720 islpir 21339 evlsval 22111 volfiniun 25583 dvmptfsum 26014 sltval2 27702 sltsolem1 27721 nosepnelem 27725 nolt02o 27741 axlowdimlem13 28970 usgredg2v 29245 issubgr 29289 clwlkcompbp 29803 pjneli 31743 indifbi 32540 madjusmdetlem1 33827 breprexp 34649 bnj553 34913 bnj1253 35032 gonanegoal 35358 goalrlem 35402 goalr 35403 fmlasucdisj 35405 satffunlem 35407 satffunlem1lem1 35408 satffunlem2lem1 35410 altopthsn 35963 bj-2upleq 37014 relowlpssretop 37366 iscrngo2 38005 extid 38312 cdleme18d 40298 fphpd 42832 oenassex 43336 rp-fakeuninass 43534 relexp0eq 43719 comptiunov2i 43724 clsk1indlem1 44063 ntrclskb 44087 onfrALTlem5 44567 onfrALTlem4 44568 onfrALTlem5VD 44910 onfrALTlem4VD 44911 dvnprodlem3 45968 sge0xadd 46455 reuabaiotaiota 47104 rrx2linest 48668 fucofvalne 49043 | 
| Copyright terms: Public domain | W3C validator |