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 2825 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶)) | |
2 | eqeq2 2833 | . 2 ⊢ (𝐶 = 𝐷 → (𝐵 = 𝐶 ↔ 𝐵 = 𝐷)) | |
3 | 1, 2 | sylan9bb 510 | 1 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 = wceq 1528 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-9 2115 ax-ext 2793 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-cleq 2814 |
This theorem is referenced by: eqeq12d 2837 eqeqan12dALT 2839 funopg 6383 eqfnfv 6795 2f1fvneq 7009 riotaeqimp 7129 soxp 7814 tfr3 8026 xpdom2 8601 dfac5lem4 9541 kmlem9 9573 sornom 9688 zorn2lem6 9912 elwina 10097 elina 10098 bcn1 13663 summo 15064 prodmo 15280 vdwlem12 16318 pslem 17806 gaorb 18377 gsumval3eu 18955 ringinvnz1ne0 19273 cygznlem3 20646 mat1ov 20987 dmatmulcl 21039 scmatscmiddistr 21047 scmatscm 21052 1mavmul 21087 chmatval 21367 dscmet 23111 dscopn 23112 iundisj2 24079 wlkres 27380 wlkp1lem8 27390 1wlkdlem4 27847 frgr2wwlk1 28036 iundisj2f 30269 iundisj2fi 30447 pfxwlk 32268 erdszelem9 32344 satfv0 32503 satfv0fun 32516 satffunlem 32546 satffunlem1lem1 32547 satffunlem2lem1 32549 fununiq 32910 sltval2 33061 bj-opelidb 34337 bj-ideqgALT 34343 bj-idreseq 34347 bj-idreseqb 34348 bj-ideqg1 34349 bj-ideqg1ALT 34350 unirep 34871 eqeqan2d 35386 csbfv12gALTVD 41113 prproropf1olem4 43515 paireqne 43520 prmdvdsfmtnof1lem2 43594 uspgrsprf1 43869 |
Copyright terms: Public domain | W3C validator |