![]() |
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 2747 | 1 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 = wceq 1542 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 df-cleq 2725 |
This theorem is referenced by: eqeqan12dALT 2755 funopg 6539 eqfnfv 6986 2f1fvneq 7211 riotaeqimp 7344 soxp 8065 tfr3 8349 xpdom2 9017 dfac5lem4 10070 kmlem9 10102 sornom 10221 zorn2lem6 10445 elwina 10630 elina 10631 bcn1 14222 summo 15610 prodmo 15827 vdwlem12 16872 pslem 18469 gaorb 19095 gsumval3eu 19689 ringinvnz1ne0 20024 cygznlem3 20999 mat1ov 21820 dmatmulcl 21872 scmatscmiddistr 21880 scmatscm 21885 1mavmul 21920 chmatval 22201 dscmet 23951 dscopn 23952 iundisj2 24936 sltval2 27027 wlkres 28667 wlkp1lem8 28677 1wlkdlem4 29133 frgr2wwlk1 29322 iundisj2f 31561 iundisj2fi 31754 pfxwlk 33781 erdszelem9 33857 satfv0 34016 satfv0fun 34029 satffunlem 34059 satffunlem1lem1 34060 satffunlem2lem1 34062 fununiq 34406 bj-opelidb 35673 bj-ideqgALT 35679 bj-idreseq 35683 bj-idreseqb 35684 bj-ideqg1 35685 bj-ideqg1ALT 35686 unirep 36222 eqeqan2d 36743 csbfv12gALTVD 43273 fcoresf1 45393 imasetpreimafvbijlemf1 45686 prproropf1olem4 45788 paireqne 45793 prmdvdsfmtnof1lem2 45867 uspgrsprf1 46139 mndtcbas2 47199 |
Copyright terms: Public domain | W3C validator |