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.) |
Ref | Expression |
---|---|
eqeq12 | ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqeq1 2823 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶)) | |
2 | eqeq2 2831 | . 2 ⊢ (𝐶 = 𝐷 → (𝐵 = 𝐶 ↔ 𝐵 = 𝐷)) | |
3 | 1, 2 | sylan9bb 512 | 1 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 = wceq 1531 |
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 1905 ax-6 1964 ax-7 2009 ax-9 2118 ax-ext 2791 |
This theorem depends on definitions: df-bi 209 df-an 399 df-ex 1775 df-cleq 2812 |
This theorem is referenced by: eqeq12d 2835 eqeqan12dALT 2837 funopg 6382 eqfnfv 6795 2f1fvneq 7010 riotaeqimp 7132 soxp 7815 tfr3 8027 xpdom2 8604 dfac5lem4 9544 kmlem9 9576 sornom 9691 zorn2lem6 9915 elwina 10100 elina 10101 bcn1 13665 summo 15066 prodmo 15282 vdwlem12 16320 pslem 17808 gaorb 18429 gsumval3eu 19016 ringinvnz1ne0 19334 cygznlem3 20708 mat1ov 21049 dmatmulcl 21101 scmatscmiddistr 21109 scmatscm 21114 1mavmul 21149 chmatval 21429 dscmet 23174 dscopn 23175 iundisj2 24142 wlkres 27444 wlkp1lem8 27454 1wlkdlem4 27911 frgr2wwlk1 28100 iundisj2f 30332 iundisj2fi 30512 pfxwlk 32363 erdszelem9 32439 satfv0 32598 satfv0fun 32611 satffunlem 32641 satffunlem1lem1 32642 satffunlem2lem1 32644 fununiq 33005 sltval2 33156 bj-opelidb 34436 bj-ideqgALT 34442 bj-idreseq 34446 bj-idreseqb 34447 bj-ideqg1 34448 bj-ideqg1ALT 34449 unirep 34980 eqeqan2d 35495 csbfv12gALTVD 41224 imasetpreimafvbijlemf1 43555 prproropf1olem4 43659 paireqne 43664 prmdvdsfmtnof1lem2 43738 uspgrsprf1 44013 |
Copyright terms: Public domain | W3C validator |