| 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 2751 | 1 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-cleq 2729 |
| This theorem is referenced by: eqeqan12dALT 2759 funopg 6600 eqfnfv 7051 2f1fvneq 7280 riotaeqimp 7414 soxp 8154 tfr3 8439 xpdom2 9107 dfac5lem4 10166 dfac5lem4OLD 10168 kmlem9 10199 sornom 10317 zorn2lem6 10541 elwina 10726 elina 10727 bcn1 14352 summo 15753 prodmo 15972 vdwlem12 17030 pslem 18617 gaorb 19325 gsumval3eu 19922 ringinvnz1ne0 20297 cygznlem3 21588 mat1ov 22454 dmatmulcl 22506 scmatscmiddistr 22514 scmatscm 22519 1mavmul 22554 chmatval 22835 dscmet 24585 dscopn 24586 iundisj2 25584 sltval2 27701 wlkres 29688 wlkp1lem8 29698 1wlkdlem4 30159 frgr2wwlk1 30348 iundisj2f 32603 iundisj2fi 32799 pfxwlk 35129 erdszelem9 35204 satfv0 35363 satfv0fun 35376 satffunlem 35406 satffunlem1lem1 35407 satffunlem2lem1 35409 fununiq 35769 bj-opelidb 37153 bj-ideqgALT 37159 bj-idreseq 37163 bj-idreseqb 37164 bj-ideqg1 37165 bj-ideqg1ALT 37166 unirep 37721 eqeqan2d 38237 csbfv12gALTVD 44919 fcoresf1 47081 imasetpreimafvbijlemf1 47391 prproropf1olem4 47493 paireqne 47498 prmdvdsfmtnof1lem2 47572 uspgrsprf1 48063 oppcendc 48906 mndtcbas2 49180 |
| Copyright terms: Public domain | W3C validator |