![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > eqeq12 | Structured version Visualization version GIF version |
Description: Equality relationship among four classes. (Contributed by NM, 3-Aug-1994.) (Proof shortened by Wolf Lammen, 23-Oct-2024.) |
Ref | Expression |
---|---|
eqeq12 | ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 22 | . 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵) | |
2 | id 22 | . 2 ⊢ (𝐶 = 𝐷 → 𝐶 = 𝐷) | |
3 | 1, 2 | eqeqan12d 2740 | 1 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 = wceq 1534 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1775 df-cleq 2718 |
This theorem is referenced by: eqeqan12dALT 2748 funopg 6593 eqfnfv 7044 2f1fvneq 7275 riotaeqimp 7407 soxp 8143 tfr3 8429 xpdom2 9105 dfac5lem4 10169 kmlem9 10201 sornom 10320 zorn2lem6 10544 elwina 10729 elina 10730 bcn1 14330 summo 15721 prodmo 15938 vdwlem12 16994 pslem 18597 gaorb 19301 gsumval3eu 19902 ringinvnz1ne0 20279 cygznlem3 21567 mat1ov 22441 dmatmulcl 22493 scmatscmiddistr 22501 scmatscm 22506 1mavmul 22541 chmatval 22822 dscmet 24572 dscopn 24573 iundisj2 25569 sltval2 27686 wlkres 29607 wlkp1lem8 29617 1wlkdlem4 30073 frgr2wwlk1 30262 iundisj2f 32510 iundisj2fi 32699 pfxwlk 34951 erdszelem9 35027 satfv0 35186 satfv0fun 35199 satffunlem 35229 satffunlem1lem1 35230 satffunlem2lem1 35232 fununiq 35592 bj-opelidb 36859 bj-ideqgALT 36865 bj-idreseq 36869 bj-idreseqb 36870 bj-ideqg1 36871 bj-ideqg1ALT 36872 unirep 37415 eqeqan2d 37933 csbfv12gALTVD 44575 fcoresf1 46684 imasetpreimafvbijlemf1 46976 prproropf1olem4 47078 paireqne 47083 prmdvdsfmtnof1lem2 47157 uspgrsprf1 47524 mndtcbas2 48410 |
Copyright terms: Public domain | W3C validator |