![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eqeqan12d | GIF version |
Description: A useful inference for substituting definitions into an equality. (Contributed by NM, 9-Aug-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
Ref | Expression |
---|---|
eqeqan12d.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
eqeqan12d.2 | ⊢ (𝜓 → 𝐶 = 𝐷) |
Ref | Expression |
---|---|
eqeqan12d | ⊢ ((𝜑 ∧ 𝜓) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqeqan12d.1 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | eqeqan12d.2 | . 2 ⊢ (𝜓 → 𝐶 = 𝐷) | |
3 | eqeq12 2202 | . 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷)) | |
4 | 1, 2, 3 | syl2an 289 | 1 ⊢ ((𝜑 ∧ 𝜓) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 = wceq 1364 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1458 ax-gen 1460 ax-4 1521 ax-17 1537 ax-ext 2171 |
This theorem depends on definitions: df-bi 117 df-cleq 2182 |
This theorem is referenced by: eqeqan12rd 2206 eqfnfv 5634 eqfnfv2 5635 f1mpt 5793 xpopth 6202 f1o2ndf1 6254 ecopoveq 6657 xpdom2 6858 djune 7108 addpipqqs 7400 enq0enq 7461 enq0sym 7462 enq0tr 7464 enq0breq 7466 preqlu 7502 cnegexlem1 8163 neg11 8239 subeqrev 8364 cnref1o 9682 xneg11 9866 modlteq 10430 sq11 10627 qsqeqor 10665 fz1eqb 10805 cj11 10949 sqrt11 11083 sqabs 11126 recan 11153 reeff1 11743 efieq 11778 xpsff1o 12828 ismhm 12928 tgtop11 14053 ioocosf1o 14752 |
Copyright terms: Public domain | W3C validator |