Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > eqeq12 | Structured version Visualization version GIF version |
Description: Equality relationship among 4 classes. (Contributed by NM, 3-Aug-1994.) |
Ref | Expression |
---|---|
eqeq12 | ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqeq1 2614 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶)) | |
2 | eqeq2 2621 | . 2 ⊢ (𝐶 = 𝐷 → (𝐵 = 𝐶 ↔ 𝐵 = 𝐷)) | |
3 | 1, 2 | sylan9bb 732 | 1 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 ∧ wa 383 = wceq 1475 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-an 385 df-cleq 2603 |
This theorem is referenced by: eqeq12d 2625 eqeqan12dALT 2627 funopg 5836 eqfnfv 6219 soxp 7177 tfr3 7382 xpdom2 7940 dfac5lem4 8832 kmlem9 8863 sornom 8982 zorn2lem6 9206 elwina 9387 elina 9388 bcn1 12962 summo 14295 prodmo 14505 vdwlem12 15534 pslem 17029 gaorb 17563 gsumval3eu 18128 ringinvnz1ne0 18415 cygznlem3 19737 mat1ov 20073 dmatmulcl 20125 scmatscmiddistr 20133 scmatscm 20138 1mavmul 20173 chmatval 20453 dscmet 22187 dscopn 22188 iundisj2 23124 usgra2wlkspthlem2 26148 constr3trllem2 26179 frg2wot1 26584 frg2woteqm 26586 iundisj2f 28785 iundisj2fi 28943 erdszelem9 30435 fununiq 30913 sltval2 31053 nofulllem5 31105 bj-elid 32262 unirep 32677 csbfv12gALTVD 38157 prmdvdsfmtnof1lem2 40035 2f1fvneq 40322 riotaeqimp 40338 1wlkres 40879 1wlkp1lem8 40889 11wlkdlem4 41307 frgr2wwlk1 41494 |
Copyright terms: Public domain | W3C validator |