![]() |
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 2776 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶)) | |
2 | eqeq2 2783 | . 2 ⊢ (𝐶 = 𝐷 → (𝐵 = 𝐶 ↔ 𝐵 = 𝐷)) | |
3 | 1, 2 | sylan9bb 502 | 1 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ wa 387 = wceq 1507 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-9 2059 ax-ext 2744 |
This theorem depends on definitions: df-bi 199 df-an 388 df-ex 1743 df-cleq 2765 |
This theorem is referenced by: eqeq12d 2787 eqeqan12dALT 2789 eqeqan1dOLDOLD 2792 funopg 6216 eqfnfv 6621 2f1fvneq 6837 riotaeqimp 6954 soxp 7622 tfr3 7833 xpdom2 8402 dfac5lem4 9340 kmlem9 9372 sornom 9491 zorn2lem6 9715 elwina 9900 elina 9901 bcn1 13482 summo 14928 prodmo 15144 vdwlem12 16178 pslem 17668 gaorb 18202 gsumval3eu 18772 ringinvnz1ne0 19059 cygznlem3 20412 mat1ov 20755 dmatmulcl 20807 scmatscmiddistr 20815 scmatscm 20820 1mavmul 20855 chmatval 21135 dscmet 22879 dscopn 22880 iundisj2 23847 wlkres 27150 wlkresOLD 27152 wlkp1lem8 27162 1wlkdlem4 27663 frgr2wwlk1 27857 iundisj2f 30100 iundisj2fi 30270 erdszelem9 32031 fununiq 32532 sltval2 32684 bj-elid 33938 unirep 34430 eqeqan2d 34947 csbfv12gALTVD 40652 prproropf1olem4 43036 paireqne 43041 prmdvdsfmtnof1lem2 43115 uspgrsprf1 43390 |
Copyright terms: Public domain | W3C validator |